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,...
| Những tác giả chính: | , |
|---|---|
| Tác giả khác: | |
| Ngôn ngữ: | en_US |
| Được phát hành: |
2005
|
| Truy cập trực tuyến: | http://hdl.handle.net/1721.1/30510 |