Specification-Guided Component-Based Synthesis from Effectful Libraries
summary
Cobalt implements Hoare-style pre/post specifications over OCaml libraries and combines spec-guided bi-directional search (backward weakest-pre to forward strongest-post) with a CDCL-style conflict learning layer that records stuck and truncated predicates to prune duplicate failing paths. It scales to a corpus of 251 functions across 48 files and 47 benchmarks; backward-only fails on 34/47, forward-only fails on 6/47, Cobalt finds 5 solutions others miss, runs about 2x faster than forward-only on average, and a no-CDCL variant is roughly 6x slower.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:04Effectful library challenges
- 3:33Why effectful components complicate synthesis
- 8:30Effect specs in Cobalt
- 13:53Backward and forward synthesis
- 20:55Conflict-driven learning
- 28:04Soundness and completeness
- 28:48Evaluation results
- 31:55Summary
- 32:38Q&A surprises
- 35:26Q&A specs
related talks
15mData-Driven Abductive Inference of Library Specifications
31mCooperative Specification via Composition Control
23mSpecifying and Verifying Future Conditions
59mTheory makes beautiful programs
20mAutomatic and Incremental Repair for Speculative Information Leaks
22mVerification Modulo Tested Library Contracts
23mStop Making LLMs Deterministic: A Spec-Driven Software Factory
01h 07mThe Cogent and Dargent approach to facilitating verified software development