Metamorph: Synthesizing Large Objects from Dafny Specifications
summary
Metamorph synthesizes long sequences of Dafny-specified API calls by replaying verifier counterexamples one step at a time and framing search as weighted A with integer programming to compute a piecewise distance metric. It limits solver context by reconstructing concrete intermediate heap states from Dafny counterexamples and uses a greedy alternative for comparison. Evaluation on linked lists, queues, arrays, binary trees, and graphs produces programs requiring up to 57 method calls, integrates with DTest*, and ships reproducible artifacts.
AI-written summary · about
chapters (8)
- 0:00Metamorph introduction
- 1:05Dafny overview
- 2:51Social network example
- 4:19Backward synthesis approach
- 6:07Distance metrics
- 7:33Evaluation vs baselines
- 9:39Results summary
- 10:20Q&A
related talks
15mAutomatic Synthesis of Data-Flow Analyzers
19mVerifying Dafny Contract Integrity
01h 02mLanguage Design meets Verifying Compilers
22mProgram Synthesis for Artifacts beyond Programs
43mEvident Code, at Scale
01h 05mVerifying Infinitely Many Programs at Once
15mUnifying Execution of Imperative Generators and Declarative Specifications
26mMeta-programming for Dummies