{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:48:13Z","timestamp":1767926893410,"version":"3.49.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2130671, CCF-2217064, CCF-2313023"],"award-info":[{"award-number":["CNS-2130671, CCF-2217064, CCF-2313023"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>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 it 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 side conditions 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.<\/jats:p>\n          <jats:p>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: Since a loop invariant often looks quite similar to the symbolic state right before the loop, our tool asks the user to express the desired loop invariant as a diff from the symbolic state before the loop, which has the potential to lead to shorter, more maintainable proofs.<\/jats:p>\n          <jats:p>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\u2019s 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 larger trusted code base can compile them with GCC.<\/jats:p>","DOI":"10.1145\/3656439","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1535-1558","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Live Verification in an Interactive Proof Assistant"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8369-9117","authenticated-orcid":false,"given":"Samuel","family":"Gruetter","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2074-7329","authenticated-orcid":false,"given":"Viktor","family":"Fukala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_3_1","unstructured":"Daniel J. Bernstein. 2006. Crit-Bit Trees. https:\/\/cr.yp.to\/critbit.html"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0314-5"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579834"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10181-1_13"},{"key":"e_1_3_2_8_1","unstructured":"Deepak L. Chaudhari and Om P. Damani. 2015. CAPS A Calculational Assistant for Programming from Specifications. https:\/\/www.cse.iitb.ac.in\/~dipakc\/CAPS\/"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Andres Erbsen Samuel Gruetter Joonwon Choi Clark Wood and Adam Chlipala. 2021. Integration Verification Across Software and Hardware for a Simple Embedded System. PLDI\u201921 (2021). https:\/\/doi.org\/10.1145\/3453483.3454065 10.1145\/3453483.3454065","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Samuel Gruetter Viktor Fukala and Adam Chlipala. 2024. Code Artifact for Live Verification in an Interactive Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.10806323 10.5281\/zenodo.10806323","DOI":"10.5281\/zenodo.10806323"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_14_1","unstructured":"Peter Lammich. 2015. The Isabelle Refinement Framework. Kolloquium Programmiersprachen (2015). https:\/\/www.complang.tuwien.ac.at\/kps2015\/proceedings\/KPS_2015_submission_13.pdf"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9437-1"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino. 2013. Developing Verified Programs with Dafny. In 2013 35th International Conference on Software Engineering (ICSE). 1488\u20131490. https:\/\/doi.org\/10.1109\/ICSE.2013.6606754 10.1109\/ICSE.2013.6606754","DOI":"10.1109\/ICSE.2013.6606754"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"key":"e_1_3_2_20_1","unstructured":"Cl\u00e9ment Pit-Claudel and Thomas Bourgeat. 2021. An Experience Report on Writing Usable DSLs in Coq. In CoqPL\u201921: The Seventh International Workshop on Coq for PL Assia Mahboubi and Amin Timany (Eds.). https:\/\/pit-claudel.fr\/clement\/papers\/koika-dsls-CoqPL21.pdf"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_3_2_22_1","unstructured":"Shaz Qadeer. 2020. ModelViewer and BVD Projects. https:\/\/github.com\/boogie-org\/boogie\/issues\/293"},{"key":"e_1_3_2_23_1","unstructured":"Thomas Tuerk. 2010. Local Reasoning about While-Loops. VSTTE 2010 (2010)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656439","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656439","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:38:52Z","timestamp":1751661532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656439"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":22,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656439"],"URL":"https:\/\/doi.org\/10.1145\/3656439","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}