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: | Gruetter, Samuel, Fukala, Viktor, Chlipala, Adam |
---|---|
Other Authors: | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
Format: | Article |
Language: | English |
Published: |
Association for Computing Machinery
2024
|
Online Access: | https://hdl.handle.net/1721.1/155515 |
Similar Items
-
Foundational Integration Verification of a Cryptographic Server
by: Erbsen, Andres, et al.
Published: (2024) -
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
by: Gross, Jason, et al.
Published: (2024) -
Specification and Verification of Strong Timing Isolation of Hardware Enclaves
by: Lau, Stella, et al.
Published: (2025) -
Elderly assisted living system
by: Muhammad Amirun Fariandie Jumri
Published: (2020) -
Untangling Mechanized Proofs
by: Pit-Claudel, Cl?ment
Published: (2025)