Certifying Synthesized Code

Abstract

Code certication is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satises certain quality properties. These proofs serve as certicates that can be checked independently. Since code certication uses the same underlying technology as program verication, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone. We address this problem by combining code certication with automatic program synthesis. Given a high-level specication, our approach simultaneously generates code and all annotations required to certify the generated code. We describe a certication extension of AutoBayes, a synthesis tool for automatically generating data analysis programs. Based on built-in domain knowledge, proof annotations are added and used to generate proof obligations that are discharged by the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator- and memory-safety on a data-classication program. For this program, our approach was faster and more precise than PolySpace, a commercial static analysis tool.