| Publication Title: |
Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| Publication Author: |
Salcianu, Alexandru |
| Additional Authors: |
Konstantine Arkoudas |
| LCS Document Number: |
MIT-LCS-TR-976 |
| Publication Date: |
12-16-2004 |
| LCS Group: |
Program Analysis |
| Additional URL: |
|
| Abstract: |
| This technical report 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 part, proven once, independent of any
specific analysis; and several analysis-specific conditions proven in Athena. |
| To obtain this publication: |
|
|
|
To purchase a printed copy of this publication please contact
MIT
Document Services.
|