NASA Ames Research Center, Code IC, Robust Software Engineering Group,

Synthesizing Certified Code

Mike Whalen, Johann Schumann, Bernd Fischer

Proc. Formal Methods Europe (FME 2002), Copenhagen, Denmark, July 22-24, 2002, Lars-Henrik Eriksson, Peter Alexander Lindsay (eds.), LNCS 2391, pp. 431-450, Springer.

Abstract

Code certification is a lightweight approach to demonstrate software quality on a formal level. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates which can be checked independently. Since code certification uses the same underlying technology as program verification, it also requires many detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding these annotations to the code is time-consuming and error-prone.

We address this problem by combining code certification with automatic program synthesis. We propose an approach to generate simultaneously, from a high-level specification, code and all annotations required to certify the generated code. Here, we describe such an extension of AutoBayes, a synthesis tool which automatically generates complex data analysis programs from compact specifications. AutoBayes contains sufficient high-level domain knowledge to generate very detailed annotations. This allows us to use a general-purpose verification condition generator to produce a set of proof obligations in first-order logic. The obligations are then discharged using the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator safety and memory safety for a generated iterative data classification program without manual annotation of the code.

Key words

formal methods, program verification, code certification, proof-carrying code, automatic program synthesis, automated theorem proving.

Contents

Download complete paper (125 KBytes, compressed PostScript)

Go to the home page of the Robust Software Engineering Group

Bernd Fischer / fisch@email.arc.nasa.gov