Enhancing Symbolic Execution with Machine-Checked Safety Proofs

Learn how to enhance symbolic execution with machine-checked safety proofs in this 21-minute conference presentation from CPP 2026. Explore a systematic approach that generates formal safety proofs for each symbolic execution analysis, addressing the challenge that modern SE engines typically consider exhaustively analyzed programs as safe without providing formal guarantees. Discover the two main components of this methodology: a formal framework connecting concrete and symbolic semantics, and an instrumentation of the SE engine that generates formal safety proofs based on this framework. Examine the implementation of a KLEE-based prototype that operates on a subset of LLVM IR with integers and generates proofs in Rocq, including preliminary experimental results showing reasonable validation times with only minor overhead on the SE engine. Gain insights into previously unknown semantic implementation issues in KLEE that were discovered during the prototype development, and understand how this approach bridges the gap between practical symbolic execution and formal verification without requiring a fully verified SE engine.