Automatic construction of hoare proofs from abstract interpretation results

Abstract

By combining program logic and static analysis, we present an automatic approach to construct program proofs to be used in Proof-Carrying Code. We use Hoare logic in representing the proofs of program properties, and the abstract interpretation in computing the program properties. This combination automatizes proof construction; an abstract interpretation automatically estimates program properties (approximate invariants) of our interest, and our proof-construction method constructs a Hoare-proof for those approximate invariants. The proof-checking side (code consumer's side) is insensitive to a specific static analysis; the assertions in the Hoare proofs are always first-order logic formulas for integers, into which we first compile the abstract interpreters' results. Both the property-compilation and the proof construction refer to the standard safety conditions that are prescribed in the abstract interpretation framework. We demonstrate this approach for a simple imperative language with an example property being the integer ranges of program variables. We prove the correctness of our approach, and analyze the size complexity of the generated proofs.