Live Verification in an Interactive Proof Assistant
summary
Prototype implements live verification after each line inside Coq, parsing polyglot C/Coq files and updating a concise symbolic state view while editing; it uses a weakest-precondition generator reworked to step forward, and requires only a small trusted kernel. Loop invariants get specified as loop-invariant diffs from the pre-loop symbolic state, reducing boilerplate; the prototype links to a verified compiler (optionally GCC for larger TCB) and the demos and case studies show the idea working end-to-end.
AI-written summary · about
chapters (13)
- 0:00Live verification assistant intro
- 2:35Goal of symbolic state tool
- 6:08Fake demo to real implementation
- 7:33Weakest precondition generators
- 10:44Forward evaluation with WP
- 11:26Deriving programs from proofs
- 13:55Proof writing like coding
- 14:36Loop invariants and simplification
- 16:42Design trade-offs and compilation
- 17:26Case studies and limitations
- 18:09Q&A on VS Code integration
- 19:34Comparison with Daphne
- 20:16Key takeaways for developers
related talks
26mIntegrating graphical proofs in Coq
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
21mIntegrating Dependency Building with Document Checking in Coq
24mA Counterexample-Guided Debugger for Non-Recursive Datalog
13mA Drag-and-Drop Proof Tactic
15mProgram Sketching with Live Bidirectional Evaluation
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
26mCodeProber: Live Compiler Exploration