AutoBayes/CC – combining program synthesis with automatic code certification – system description. (English) Zbl 1072.68597

Voronkov, Andrei (ed.), Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27–30, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43931-5). Lect. Notes Comput. Sci. 2392, 290-294 (2002).
Summary: Code certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code.
For the entire collection see [Zbl 0993.00050].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)


Full Text: Link