Trustworthy Runtime Verification via Bisimulation
summary
CopilotVerifier automatically proves that a Copilot Haskell stream monitor and its compiled C (Clang→LLVM) output produce equivalent observable behavior by reducing bisimulation to extensional equality and discharging generated VCs with the Crucible symbolic execution engine and the What4 SMT interface. It runs as a translation‑validation pass next to copilot‑c99, finds crash‑equivalence (or inability to crash), detects 10 real compiler bugs, verifies the entire Copilot test corpus, and ships with caveats for floating‑point reasoning.
AI-written summary · about
chapters (19)
- 0:00Compiler verification project intro
- 1:25Verification constraints and success
- 2:28Bisimulation program equivalence proof
- 4:57Co-Pilot stream language overview
- 8:28Compiling Co-Pilot to C
- 10:11Translation validation choice
- 13:00Co-Pilot Verifier equivalence proof
- 16:35Simulation for extensional equality
- 19:03Floating-point verification handling
- 20:06NASA auditing proof presentation
- 20:49Higher safety classification plans
- 21:32Q&A on verification failures
- 23:17SMT solver alternatives
- 24:19Compiler bugs vs tool limits
- 25:02External specs future work
- 26:08NASA safety classification levels
- 26:53Control flow graphs in What4
- 27:56Random testing for compiler bugs
- 28:59Bisimulation undecidability limits
related talks
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
47mHow to trust a verified program?
27mC4: verified transactional objects
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
01h 05mVerifying Infinitely Many Programs at Once
28mGradual Verification: Assuring Software Incrementally
22mVerification Modulo Tested Library Contracts
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...