+Synthesis Projects & Applications

Certifiable Synthesis

Formal certifcation is based on the idea that a mathematical proof of some property of a piece of software can be regarded as a
certifcate of correctness which, in principle, can be subjected to external scrutiny. In practice, however, proofs themselves are unlikely to be of
much interest to engineers. Nevertheless, it is possible to use the information obtained from a mathematical analysis of software to produce a
detailed textual justifcation of correctness. In this paper, we describe an
approach to generating textual explanations from automatically generated proofs of program safety, where the proofs are of compliance with an
explicit safety policy that can be varied. Key to this is tracing proof obligations back to the program, and we describe a tool which implements
this to certify code auto-generated by AutoBayes and AutoFilter, program synthesis systems under development at the NASA Ames Research
Center. Our approach is a step towards combining formal certifcation
with traditional certifcation methods.

Code generators for realistic application domains are not directly verifable in practice. In the certifable code generation approach the generator is extended to generate logical annotations (i.e., pre and postconditions and loop invariants) along with the programs, allowing fully automated program proofs of different safety properties. However, this requires access to the generator sources, and remains diffcult to implement and maintain because the annotations are cross-cutting concerns, both on the object-level (i.e., in the generated code) and on the meta-level (i.e., in the generator). Here we describe a new generic post-generation annotation inference algorithm that circumvents these problems. We exploit the fact that the output of a code generator is highly idiomatic, so that patterns can be used to describe all code constructs that require annotations. The patterns are specific to the idioms of the targeted code generator and to the safety property to be shown, but the algorithm itself remains generic. It is based on a pattern matcher used to identify instances of the idioms and build a property specifc abstracted control flow graph, and a graph traversal that follows the paths from the use nodes backwards to all corresponding defnitions, annotating the statements along these paths. This core is instantiated for two generators and successfully applied to automatically certify initialization safety for a range of generated programs.

*Reviewed 2012*