Synthesizing Contracts Correct Modulo a Test Generator
summary
Approach synthesizes tight contracts as decision trees and integrates a SyGuS-based learner (CVC4Sy) with the Pex test generator to get guarantees modulo a test generator. Implementation precis targets C# libraries (.NET Core, QuickGraph), synthesizes quantifier-free summaries, proves per-round termination and that if the counterexample loop finishes the summary is both safe and tight, and reports that about 82% of generated summaries are truly safe versus Daikon while producing more disjunctive, stronger contracts.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:24Contracts are Useful
- 1:25Contract Synthesis modulo a Test Generator in Oo
- 2:13Learning Framework for Contract Summaries
- 3:16Example: Features, Logics and Counterexamples (samples)
- 4:50Formalizing Strength of Contract Summaries
- 7:03Contract Synthesizer: A Learner of Tight Summaries
- 9:17Learning Framework for Contract (summary) Synthesis in oo
- 9:46Implementation and Evaluation
- 10:33How effectively can Precis learn Truly Safe summaries?
- 11:10How effectively can Precis learn strong summaries?
- 12:01How effective is Precis in comparison to Daikon AL
- 13:05Conclusions
related talks
22mVerification Modulo Tested Library Contracts
21mTrace-Guided Synthesis of Effectful Test Generators
22mProgram Synthesis for Artifacts beyond Programs
19mCovering All the Bases: Type-Based Verification of Test Input Generators
30mGenerating Conforming Programs With Xsmith
19mSynthesizing Specifications
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
40mYou are a Program Synthesizer