Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses
This technical report describes our experience using the interactive theorem proverAthena for proving the correctness of abstract interpretation-based dataflow analyses.For each analysis, our methodology requires the analysis designer to formallyspecify the property lattice, the transfer functions,...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30510 |