Machine-Checkable Correctness Proofs for
Intra-procedural Dataflow Analyses
Alexandru Salcianu, Konstantine Arkoudas
MIT, USA
This paper describes our experience using the interactive theorem prover Athena for proving the correctness of abstract interpretation-based dataflow analyses. For each analysis, our methodology requires the analysis designer to formally specify the property lattice, the transfer functions, and the desired modeling relation between the concrete program states and the results computed by the analysis. The goal of the correctness proof is to prove that the desired modeling relation holds; the proof allows the analysis clients to rely on the modeling relation for their own correctness. To reduce the complexity of the proofs, we separate the proof of each dataflow analysis into two parts: a generic one --- proven on paper, once and for all --- and several analysis-specific conditions --- proven in Athena.