Structural abstract interpretation, A formal study using Coq

TL;DR

This paper formalizes an abstract interpreter within Coq, using inductive types and structural recursion, and proves its correctness relative to a Hoare logic, enhancing reliability in program analysis.

Contribution

It introduces a formal method for specifying and verifying abstract interpreters in Coq, bridging theoretical foundations with practical correctness proofs.

Findings

Successfully formalized an abstract interpreter in Coq

Proved the interpreter's correctness using Hoare logic

Demonstrated the approach's potential for reliable program analysis

Abstract

interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory based theorem prover Coq, using inductive types for syntax and structural recursive programming for the abstract interpreter's kernel. The abstract interpreter can then be proved correct with respect to a Hoare logic for the programming language.