Synthesis and Verification for All
summary
Rosette is a Racket-based language that compiles interpreters to solver constraints via a symbolic virtual machine, exposing six solver-aware constructs so a ten-line interpreter for a toy BV assembly gets verification, debugging and synthesis for free. The workflow uses define-symbolic/assert/verify to find counterexamples, isolate minimal faulty expressions, and fill holes with synthesized code. The tools find a real safety bug in an EPICS radiotherapy controller, power an automated K–12 algebra tutor pipeline, and enable a superoptimizer with up to 82% ARM speedup.
AI-written summary · about
chapters (12)
- 0:00Start
- 3:41A little programming for everyone
- 11:22Programming ...
- 12:35Programming with a solver-aided tool
- 19:47The standard (hard) way to build a tool
- 20:09A new, easy way to build tools
- 22:04Layers of languages
- 26:23Layers of solver-aided languages
- 27:30Anatomy of a solver-aided host language
- 29:56A tiny example SDSLI ROSETTE
- 47:13Recent applications of ROSETTE: Enlearn
- 48:22Recent applications of ROSETTE: Greenthumb
related talks
31mSynthesizing Evidence of Emergent Computation
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
19mLoop Rerolling for Hardware Decompilation
19mAutomated Verification of Fundamental Algebraic Laws
49mRoslyn for the rest of us
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
21mSynthesizing Formal Semantics from Executable Interpreters
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...