Live Verification in an Interactive Proof Assistant
We present a prototype for a tool that enables programmers to verify their code as they write it in real-time. After each line of code that the programmer writes, the tool tells the programmer whether it was able to prove absence of undefined behavior so far, and displays a concise representation o...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery
2024
|
| Online Access: | https://hdl.handle.net/1721.1/155515 |
| _version_ | 1824458060483002368 |
|---|---|
| author | Gruetter, Samuel Fukala, Viktor Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Gruetter, Samuel Fukala, Viktor Chlipala, Adam |
| author_sort | Gruetter, Samuel |
| collection | MIT |
| description | We present a prototype for a tool that enables programmers to verify their code as they write it in real-time.
After each line of code that the programmer writes, the tool tells the programmer whether it was able to prove absence of undefined behavior so far, and displays a concise representation of the symbolic state of the program right after the added line.
The user can then either write the next line of code, or if needed or desired, write a specially marked comment that provides hints on how to solve sideconditions, or on how to represent the symbolic state more nicely.
Once the programmer has finished writing the program, it is already verified with a mathematical correctness proof.
Other tools providing real-time feedback already exist, but ours is the first one that only relies on a small trusted proof checker and that provides a concise summary of the symbolic state at the point in the program currently being edited, as opposed to only indicating whether user-stated assertions or postconditions hold.
Program verification requires loop invariants, which are hard to find and tedious to spell out.
We explore a middle ground in the design space between the two extremes of requiring users to spell out loop invariants manually and attempting to infer loop invariants automatically:
Based on the observation that a loop invariant often looks quite similar to the symbolic state right before the loop, our tool asks users to express the desired loop invariant as a diff from the symbolic state before the loop, which has the potential to lead to less verbose and more maintainable proofs.
We prototyped our technique in the interactive proof assistant Coq, so our framework creates machine-checked proofs that the developed functions satisfy their specifications when executed according to the formal semantics of the source language.
Using a verified compiler proven against the same source-language semantics, we can ensure that the behavior of the compiled program matches the program's behavior as represented by the framework during the proof.
Additionally, since our polyglot source files can be viewed as Coq or C files at the same time, users willing to accept a bigger trusted code base can compile them with GCC. |
| first_indexed | 2024-09-23T11:00:52Z |
| format | Article |
| id | mit-1721.1/155515 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2025-02-19T04:19:53Z |
| publishDate | 2024 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | mit-1721.1/1555152024-12-21T05:53:44Z Live Verification in an Interactive Proof Assistant Gruetter, Samuel Fukala, Viktor Chlipala, Adam Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science We present a prototype for a tool that enables programmers to verify their code as they write it in real-time. After each line of code that the programmer writes, the tool tells the programmer whether it was able to prove absence of undefined behavior so far, and displays a concise representation of the symbolic state of the program right after the added line. The user can then either write the next line of code, or if needed or desired, write a specially marked comment that provides hints on how to solve sideconditions, or on how to represent the symbolic state more nicely. Once the programmer has finished writing the program, it is already verified with a mathematical correctness proof. Other tools providing real-time feedback already exist, but ours is the first one that only relies on a small trusted proof checker and that provides a concise summary of the symbolic state at the point in the program currently being edited, as opposed to only indicating whether user-stated assertions or postconditions hold. Program verification requires loop invariants, which are hard to find and tedious to spell out. We explore a middle ground in the design space between the two extremes of requiring users to spell out loop invariants manually and attempting to infer loop invariants automatically: Based on the observation that a loop invariant often looks quite similar to the symbolic state right before the loop, our tool asks users to express the desired loop invariant as a diff from the symbolic state before the loop, which has the potential to lead to less verbose and more maintainable proofs. We prototyped our technique in the interactive proof assistant Coq, so our framework creates machine-checked proofs that the developed functions satisfy their specifications when executed according to the formal semantics of the source language. Using a verified compiler proven against the same source-language semantics, we can ensure that the behavior of the compiled program matches the program's behavior as represented by the framework during the proof. Additionally, since our polyglot source files can be viewed as Coq or C files at the same time, users willing to accept a bigger trusted code base can compile them with GCC. 2024-07-08T19:03:44Z 2024-07-08T19:03:44Z 2024-06-20 2024-07-01T07:59:10Z Article http://purl.org/eprint/type/JournalArticle 2475-1421 https://hdl.handle.net/1721.1/155515 Gruetter, Samuel, Fukala, Viktor and Chlipala, Adam. 2024. "Live Verification in an Interactive Proof Assistant." Proceedings of the ACM on Programming Languages, 8 (PLDI). PUBLISHER_CC en 10.1145/3656439 Proceedings of the ACM on Programming Languages Creative Commons Attribution https://creativecommons.org/licenses/by/4.0/ The author(s) application/pdf Association for Computing Machinery Association for Computing Machinery |
| spellingShingle | Gruetter, Samuel Fukala, Viktor Chlipala, Adam Live Verification in an Interactive Proof Assistant |
| title | Live Verification in an Interactive Proof Assistant |
| title_full | Live Verification in an Interactive Proof Assistant |
| title_fullStr | Live Verification in an Interactive Proof Assistant |
| title_full_unstemmed | Live Verification in an Interactive Proof Assistant |
| title_short | Live Verification in an Interactive Proof Assistant |
| title_sort | live verification in an interactive proof assistant |
| url | https://hdl.handle.net/1721.1/155515 |
| work_keys_str_mv | AT gruettersamuel liveverificationinaninteractiveproofassistant AT fukalaviktor liveverificationinaninteractiveproofassistant AT chlipalaadam liveverificationinaninteractiveproofassistant |