Certifying Automatically Generated Code

Bernd Fischer

Abstract: Automatic code generation has the potential to increase both productivity and reliability of software development. Its practical use in safety-critical domains, however, is limited because reliable approaches based on correct-by-construction arguments don't scale, and scalable approaches based on template programming techniques are not reliable.

We have developed a schema-based synthesis approach which is both scalable and allows a property-oriented certification of the synthesized programs. Our basic principles are: (1) trustworthiness of the generator is reduced to the safety of each individual generated program; (2) program safety is defined as adherence to an explicitly formulated safety policy; (3) the safety policy is formalized by a collection of logical program properties; (4) Hoare-style program verification is used to show that each generated program satisfies the required properties; (5) the code generator itself is extended to automatically produce the code annotations required for verification. Our approach is feasible because the code generator has full knowledge about the program under construction and about the properties to be verified. It can thus generate all auxiliary code annotations a theorem prover needs to discharge all emerging verification obligations fully automatically.

In this talk, I will discuss some details of the certification techniques and will demonstrate our certifable synthesis system.