Synthesizing contracts correct modulo a test generator
Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, Tao Xie
Abstract
We present an approach to learn contracts for object-oriented programs where guarantees of correctness of the contracts are made with respect to a test generator. Our contract synthesis approach is based on a novel notion of tight contracts and an online learning algorithm that works in tandem with a test generator to synthesize tight contracts. We implement our approach in a tool called Precis and evaluate it on a suite of programs written in C#, studying the safety and strength of the synthesized contracts, and compare them to those synthesized by Daikon.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 7f83ebd8-c217-496e-8156-9f1500a17093Cited by top-tier papers7
- Synthesizing abstract transformersPankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni, Thomas W. Reps et al.OOPSLA 2022 · 21 citations
- Synthesizing SpecificationsKanghee Park, Loris D'Antoni, Thomas W. RepsOOPSLA 2023 · 9 citations
- Languages with Decidable Learning: A Meta-theoremPaul Krogmeier, P. MadhusudanOOPSLA 2023 · 4 citations
- Inductive Synthesis of Inductive Heap PredicatesZiyi Yang, Ilya SergeyOOPSLA 2025 · 1 citation
- Verification Modulo Tested Library ContractsAbhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza et al.PLDI 2026 · 1 citation
Builds on5
- Evolutionary improvement of assertion oraclesValerio Terragni, Gunel Jahangirova, Paolo Tonella, Mauro PezzèFSE 2020 · 50 citations
- C2S: translating natural language comments to formal program specificationsJuan Zhai, Yu Shi, Minxue Pan, Guian Zhou et al.FSE 2020 · 44 citations
- Verifying and improving Halide's term rewriting system with program synthesisJulie L. Newcomb, Andrew Adams, Steven Johnson, Rastislav Bodík et al.OOPSLA 2020 · 21 citations
- Unifying execution of imperative generators and declarative specificationsPengyu Nie, Marinela Parovic, Zhiqiang Zang, Sarfraz Khurshid et al.OOPSLA 2020 · 7 citations
- EvoSpex: An Evolutionary Algorithm for Learning PostconditionsFacundo Molina, Pablo Ponzio, Nazareno Aguirre, Marcelo F. FriasICSE 2021
Related papers
- Perception Contracts for Safety of ML-Enabled SystemsAngello Astorga, Chiao Hsieh, P. Madhusudan, Sayan MitraOOPSLA 2023 · 18 citations
- Concord: Learning Network Configuration ContractsRyan Beckett, Francis Y. Yan, Raghunadha Reddy Pocha, Vineesh V. Raj et al.EuroSys 2026
- Almost correct invariants: synthesizing inductive invariants by fuzzing proofsSumit Lahiri, Subhajit RoyISSTA 2022 · 18 citations
- Learning Contract Invariants Using Reinforcement LearningJunrui Liu, Yanju Chen, Bryan Tan, Isil Dillig et al.ASE 2022 · 17 citations
- Exploring the Learnability of Program Synthesizers by Novice ProgrammersDhanya Jayagopal, Justin Lubin, Sarah E. ChasinsUIST 2022 · 40 citations
