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 |
| _version_ | 1811094976006717440 |
|---|---|
| author | Salcianu, Alexandru Arkoudas, Konstantine |
| author2 | Program Analysis |
| author_facet | Program Analysis Salcianu, Alexandru Arkoudas, Konstantine |
| author_sort | Salcianu, Alexandru |
| collection | MIT |
| description | 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, and the desired modeling relationbetween the concrete program states and the results computed by the analysis. Thegoal 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 owncorrectness. To reduce the complexity of the proofs, we separate the proof of eachdataflow analysis into two parts: a generic part, proven once, independent of anyspecific analysis; and several analysis-specific conditions proven in Athena. |
| first_indexed | 2024-09-23T16:08:32Z |
| id | mit-1721.1/30510 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:08:32Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/305102019-04-12T08:37:37Z Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses Salcianu, Alexandru Arkoudas, Konstantine Program Analysis 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, and the desired modeling relationbetween the concrete program states and the results computed by the analysis. Thegoal 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 owncorrectness. To reduce the complexity of the proofs, we separate the proof of eachdataflow analysis into two parts: a generic part, proven once, independent of anyspecific analysis; and several analysis-specific conditions proven in Athena. 2005-12-22T02:19:45Z 2005-12-22T02:19:45Z 2004-12-16 MIT-CSAIL-TR-2004-080 MIT-LCS-TR-976 http://hdl.handle.net/1721.1/30510 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 16 p. 18540541 bytes 798716 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Salcianu, Alexandru Arkoudas, Konstantine Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| title | Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| title_full | Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| title_fullStr | Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| title_full_unstemmed | Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| title_short | Machine-Checkable Correctness Proofs forIntra-procedural Dataflow Analyses |
| title_sort | machine checkable correctness proofs forintra procedural dataflow analyses |
| url | http://hdl.handle.net/1721.1/30510 |
| work_keys_str_mv | AT salcianualexandru machinecheckablecorrectnessproofsforintraproceduraldataflowanalyses AT arkoudaskonstantine machinecheckablecorrectnessproofsforintraproceduraldataflowanalyses |