LOUD: Synthesizing Strongest and Weakest Specifications
summary
The paper presents LOUD, a logic and algorithm that synthesizes strongest L-consequences (over-approximations) and weakest L-implicants (under-approximations) for queries with existential quantifiers, using counterexample-guided quantifier instantiation to handle alternating quantifiers. An implementation, ASPIRE, issues Sketch queries (bounded soundness) and finds specifications that describe nondeterminism and concurrency, extract strategy conditions for two-player games, and identifies the worst-case quicksort pattern (reverse-sorted input). The approach builds on Spyro/Spiral, produces sound-and-precise expressible properties within the chosen assertion language, and scales with solver limits.
AI-written summary · about
chapters (7)
- 0:00LOUD framework intro
- 1:49Single specs are insufficient
- 3:57Safety versus reachability
- 6:07Synthesizing approximations
- 9:00LOUD in practice
- 11:30Conclusion and future
- 12:53Q&A
related talks
22mCounterexample-Guided Inference of Modular Specifications
29mSynthesizing Axiomatizations using Logic Learning
16mInterpolation and Quantifiers in Ortholattices
29mQuantitative strongest post: a calculus for reasoning about the flow of quantitative inform
01h 04mKnowledge Compilation for Quantification and Synthesis
17mCalculational design of Incorrectness Separation Logic
31mLetting users do the undecidable: lessons from program synthesis
32mA mechanised and constructive reverse analysis of soundness and completeness of b...