Synthesizing Formal Semantics from Executable Interpreters
summary
Given a grammar and a closed-box interpreter the system Synantic synthesizes inductive, syntax-directed semantics as Constrained-Horn Clauses via a CEGIS loop that lowers rule synthesis to many SyGuS-backed expression problems (uses SyGuS and CVC5, implemented in Scala). It derives one rule per syntactic construct, verifies each candidate against interpreter traces, converges on 14 benchmark interpreters within 20 minutes, and uncovers a regex-semantics bug whose fix yields a 1.2x speedup.
AI-written summary · about
chapters (11)
- 0:00Formal semantics synthesis
- 1:07Key idea behind synthesis
- 3:15Semantic rules rule by rule
- 6:48Semantics for atom terms
- 8:38Non-leaf nodes and child terms
- 13:15Recursive calls and control
- 14:40Implementation and evaluation
- 15:24Effectiveness on languages
- 16:07Synthesized vs manual semantics
- 17:11Recap and future work
- 17:33Question and answer session
related talks
30mSemantics-Guided Synthesis
18mVerifying Solutions to Semantics-Guided Synthesis Problems
35mDeriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
24mTransforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
31mLetting users do the undecidable: lessons from program synthesis
14mOne Down, 699 to Go: or, synthesising compositional desugarings