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,...
| Hlavní autoři: | , |
|---|---|
| Další autoři: | |
| Jazyk: | en_US |
| Vydáno: |
2005
|
| On-line přístup: | http://hdl.handle.net/1721.1/30510 |