Verification Modulo Tested Library Contracts
summary
Proposes a concrete pipeline that synthesizes method contracts and loop invariants by looping a generalizing CHC solver (ICE learners, decision trees, optional LLM) with a test generator; implements it as Dualis and targets clients that call large libraries (up to ~3,000 LOC). The core claim is verify the client, test the library via per-call contextual contracts that are simpler to infer. Evaluation: Seahorn solves 7/43 benchmarks, Dualis vets all synthesized contracts, adversarial suite flags 30 modular-unsynthesizable cases while producing 11 contextual false positives.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:21New verification paradigm
- 1:46Verifying client-library programs
- 3:52Formal definition of VMTLC
- 4:33Client using set library
- 7:40Client test the library approach
- 8:42Contextual contracts for guarantees
- 10:50Solver pipeline for VMTLC
- 12:34Evaluation results
- 14:41Validating synthesized contracts
- 16:25Takeaways
- 17:07Q&A
- 19:53Q&A
related talks
14mSynthesizing Contracts Correct Modulo a Test Generator
01h 05mVerifying Infinitely Many Programs at Once
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
22mTowards Modelling and Verification of Coupler Behaviour in Climate Models
15mModular Verification of Op-Based CRDTs in Separation Logic
30mTrustworthy Runtime Verification via Bisimulation
46mFrom Chaos to Cohesion: Building Modular Monoliths in the Real World
01h 02mLanguage Design meets Verifying Compilers