Foundational Multi-Modal Program Verifiers

on YouTube ↗24m

" summary

Paper presents a framework implemented in Lean implementation that provides a library of monad transformers for state, divergence, exceptions and nondeterminism and an ordered monad transformer algebra that automatically derives weakest preconditions and SMT-friendly verification conditions. Generated VCs are discharged by SMT + interactive fallback, with proof reconstruction. The authors instantiate the framework to produce two foundational multi-modal verifiers, Veil and Velvet, and mechanically verify several non-trivial case studies; artifacts and benchmarks are available.

AI-written summary · about

" chapters (14)

1. 0:00Foundational multimodal verifiers
2. 1:01Program verification tools
3. 3:10Middle ground in verification
4. 4:11Verification frameworks design
5. 6:37Verifier for money managing programs
6. 10:09Loops and termination verification
7. 12:56Exceptions and nondeterminism
8. 15:29Loom beyond monads
9. 17:57Loom's ecosystem and realistic verifiers
10. 19:03Q&A
11. 21:11Effect types vs monad transformer algebra
12. 22:13Choosing and ordering monads
13. 22:55Handling non-terminating programs
14. 24:00Separation logic compatibility