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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Seo, S., Yang, H., & Yi, K. (2003). Automatic construction of Hoare proofs from abstract interpretation results. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2895, 230–245. https://doi.org/10.1007/978-3-540-40018-9_16
Mendeley helps you to discover research relevant for your work.