Unifying Execution of Imperative Generators and Declarative Specifications
summary
Deuterium implements executable contracts as Java code combining an imperative generator that builds the solution backbone and a declarative spec in 2H that fills missing values; it ships two engines: SAT-based via Kodkod and a novel in-memory search-based solver. Evaluation uses Randoop-generated random tests and systematic method sequences across 12 data structures; the in-memory solver outperforms SAT on small workloads, SAT scales better on large ones, and generators extend solvable sequence length by about 5–20 method calls within a 30-minute timeout.
AI-written summary · about
chapters (15)
- 0:00Start
- 0:19Relation of Imperative Code and Contracts
- 1:32Limitations of Executable Contracts
- 2:40Our Contributions
- 3:49Deuterium Workflow
- 4:57Imperative Generator
- 5:49Constraint Solving Engines
- 7:06In Memory Search-Based Solver (2/2)
- 9:332H Language
- 11:21Evaluation: Workloads
- 12:18Evaluation: Framework Configurations
- 12:37Evaluation: Research Questions and Setup
- 12:49RQ1: Search-Based vs. SAT-Based Solver
- 13:33RQ2: Fusion of Generator + 2 H vs. Pure 2H
- 14:34More Content in the Paper
related talks
20mDerivative-Guided Symbolic Execution
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
47mTDD & Generative AI: A Perfect Pairing
22mVerification Modulo Tested Library Contracts
17mDafny Test Generation
43mHydra's Heads – Dmitriy Ivanov
14mSynthesizing Contracts Correct Modulo a Test Generator
21mTrace-Guided Synthesis of Effectful Test Generators