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...

Full description

Bibliographic Details
Main Authors: Gruetter, Samuel, Fukala, Viktor, Chlipala, Adam
Format: Article
Language:English
Published: Association for Computing Machinery 2024
Online Access:https://hdl.handle.net/1721.1/155515