AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification

Abstract

Code certication is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be dened 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 satises these quality properties. The proofs serve as certicates which can be checked independently, by the code consumer or by certication authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code.

Code certication can be viewed as a more practical version of traditional Hoare-style program verication. The properties to be veried are fairly simple and regular so that it is often possible to use an automated theorem prover to automatically discharge all emerging proof obligations. Usually, however, the programmer must still splice auxiliary annotations (e.g., loop invariants) into the program to facilitate the proofs. For complex properties or larger programs this quickly becomes the limiting factor for the applicability of current certication approaches.

Our work combines code certication with automatic program synthesis which makes it possible to automatically generate both the code and all necessary annotations for fully automatic certication. By generating detailed annotations, one of the biggest obstacles for code certication is removed and it becomes possible to automatically check that synthesized programs obey the desired safety properties.