An Integrated Proof Language for Imperative Programs
We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery
2010
|
| Online Access: | http://hdl.handle.net/1721.1/51822 https://orcid.org/0000-0001-8095-8523 |
| _version_ | 1826190266763051008 |
|---|---|
| author | Zee, Karen Kuncak, Viktor Rinard, Martin C. |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Zee, Karen Kuncak, Viktor Rinard, Martin C. |
| author_sort | Zee, Karen |
| collection | MIT |
| description | We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge generated proof obligations. It is designed to 1) enable developers to resolve key choice points in complex program correctness proofs, thereby enabling automated reasoning systems to successfully prove the desired correctness properties; 2) allow developers to identify key lemmas for the reasoning systems to prove, thereby guiding the reasoning systems to find an effective proof decomposition; 3) enable multiple reasoning systems to work together productively to prove a single correctness property by providing a mechanism that developers can use to divide the property into lemmas, each of which is suitable for a different reasoning system; and 4) enable developers to identify specific lemmas that the reasoning systems should use when attempting to prove other lemmas or correctness properties, thereby appropriately confining the search space so that the reasoning systems can find a proof in an acceptable amount of time.
The language includes a rich set of declarative proof constructs that enables developers to direct the reasoning systems as little or as much as they desire. Because the declarative proof statements are embedded into the program as specialized comments, they also serve as verified documentation and are a natural extension of the assertion mechanism found in most program verification systems.
We have implemented our integrated proof language in the context of a program verification system for Java and used the resulting system to verify a collection of linked data structure implementations. Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems. |
| first_indexed | 2024-09-23T08:37:37Z |
| format | Article |
| id | mit-1721.1/51822 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T08:37:37Z |
| publishDate | 2010 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | mit-1721.1/518222022-09-30T10:04:20Z An Integrated Proof Language for Imperative Programs Zee, Karen Kuncak, Viktor Rinard, Martin C. Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Rinard, Martin C. Zee, Karen Rinard, Martin C. We present an integrated proof language for guiding the actions of multiple reasoning systems as they work together to prove complex correctness properties of imperative programs. The language operates in the context of a program verification system that uses multiple reasoning systems to discharge generated proof obligations. It is designed to 1) enable developers to resolve key choice points in complex program correctness proofs, thereby enabling automated reasoning systems to successfully prove the desired correctness properties; 2) allow developers to identify key lemmas for the reasoning systems to prove, thereby guiding the reasoning systems to find an effective proof decomposition; 3) enable multiple reasoning systems to work together productively to prove a single correctness property by providing a mechanism that developers can use to divide the property into lemmas, each of which is suitable for a different reasoning system; and 4) enable developers to identify specific lemmas that the reasoning systems should use when attempting to prove other lemmas or correctness properties, thereby appropriately confining the search space so that the reasoning systems can find a proof in an acceptable amount of time. The language includes a rich set of declarative proof constructs that enables developers to direct the reasoning systems as little or as much as they desire. Because the declarative proof statements are embedded into the program as specialized comments, they also serve as verified documentation and are a natural extension of the assertion mechanism found in most program verification systems. We have implemented our integrated proof language in the context of a program verification system for Java and used the resulting system to verify a collection of linked data structure implementations. Our experience indicates that our proof language makes it possible to successfully prove complex program correctness properties that are otherwise beyond the reach of automated reasoning systems. Swiss National Science Foundation National Science Foundation DARPA 2010-02-24T21:00:42Z 2010-02-24T21:00:42Z 2009-06 2009-06 Article http://purl.org/eprint/type/ConferencePaper 0362-1340 http://hdl.handle.net/1721.1/51822 Zee, Karen, Viktor Kuncak, and Martin C. Rinard. “An integrated proof language for imperative programs.” SIGPLAN Not. 44.6 (2009): 338-351. https://orcid.org/0000-0001-8095-8523 en_US http://dx.doi.org/10.1145/1543135.1542514 ACM SIGPLAN notices : a monthly publication of the Special Interest Group on Programming Languages Attribution-Noncommercial-Share Alike 3.0 Unported http://creativecommons.org/licenses/by-nc-sa/3.0/ application/pdf Association for Computing Machinery Martin Rinard |
| spellingShingle | Zee, Karen Kuncak, Viktor Rinard, Martin C. An Integrated Proof Language for Imperative Programs |
| title | An Integrated Proof Language for Imperative Programs |
| title_full | An Integrated Proof Language for Imperative Programs |
| title_fullStr | An Integrated Proof Language for Imperative Programs |
| title_full_unstemmed | An Integrated Proof Language for Imperative Programs |
| title_short | An Integrated Proof Language for Imperative Programs |
| title_sort | integrated proof language for imperative programs |
| url | http://hdl.handle.net/1721.1/51822 https://orcid.org/0000-0001-8095-8523 |
| work_keys_str_mv | AT zeekaren anintegratedprooflanguageforimperativeprograms AT kuncakviktor anintegratedprooflanguageforimperativeprograms AT rinardmartinc anintegratedprooflanguageforimperativeprograms AT zeekaren integratedprooflanguageforimperativeprograms AT kuncakviktor integratedprooflanguageforimperativeprograms AT rinardmartinc integratedprooflanguageforimperativeprograms |