Trustworthy Runtime Verification via Bisimulation - Experience Report

Explore a 30-minute conference talk from ICFP 2023 focusing on trustworthy runtime verification through bisimulation. Delve into the CopilotVerifier, a tool that runs alongside the Copilot compiler to generate proofs of correctness for compiled output. Learn how this approach establishes equivalence between Copilot monitors and their compiled forms, ensuring identical crash behavior or crash-free operation. Discover the use of SMT-backed technology, including the Crucible symbolic execution library for LLVM and the What4 solver interface library, in creating bisimulation-based verification conditions. Gain insights into how this method significantly enhances compiler assurance at a reasonable cost, paving the way for formal assurance arguments that can convince human auditors in safety-critical domains.