Semantic Reification: A New Paradigm for Random Program Generation
summary
Claims a new semantic reification method that synthesizes a program P, input I, and expected output O from a CFG skeleton and a chosen execution path, guaranteeing the program follows that path, terminates, and is UB-free on that path. Implementation Reify (7,000 lines C++, Z3) uses symbolic function reification to make leaf functions and composes them via peephole rewriting. Results: 59 bugs found in GCC/LLVM (57 confirmed, 27 fixed), 36 wrong-code bugs; JVM port finds 3 OpenJ9 bugs; Refract IR finds 10 more in a week.
AI-written summary · about
chapters (10)
- 0:00Semantic reification intro
- 1:55Syntactic verification limits
- 3:43Arbitrary control flow testing
- 5:53Semantic reification explained
- 8:01Symbolic function creation
- 11:35Composing programs from functions
- 12:39Bug discovery results
- 14:04Implementation and scalability
- 15:09Future directions
- 15:32Q&A
related talks
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
30mSemantics-Guided Synthesis
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
01h 05mSemantic Intermediate Representations for Sound Language Interoperability
25mRecursive Program Synthesis using Paramorphisms
21mSynthesizing Formal Semantics from Executable Interpreters
15mLanguage-Parametric Reference Synthesis
34mSymbolic Execution for Randomized Programs