{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:49Z","timestamp":1780994629764,"version":"3.54.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1816615"],"award-info":[{"award-number":["CCF-1816615"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3485481","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Synthesizing contracts correct modulo a test generator"],"prefix":"10.1145","volume":"5","author":[{"given":"Angello","family":"Astorga","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shambwaditya","family":"Saha","sequence":"additional","affiliation":[{"name":"Tufts University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ahmad","family":"Dinkins","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felicia","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9782-721X","authenticated-orcid":false,"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6731-216X","authenticated-orcid":false,"given":"Tao","family":"Xie","sequence":"additional","affiliation":[{"name":"Peking University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Dependable Software Systems Engineering","author":"Alur Rajeev","year":"2015","unstructured":"Rajeev Alur , Rastislav Bod\u00edk , Eric Dallal , Dana Fisman , Pranav Garg , Garvit Juniwal , Hadas Kress-Gazit , P. Madhusudan , Milo M. K. Martin , Mukund Raghothaman , Shambwaditya Saha , Sanjit A. Seshia , Rishabh Singh , Armando Solar-Lezama , Emina Torlak , and Abhishek Udupa . 2015. Syntax-guided synthesis . In Dependable Software Systems Engineering 2015 . Rajeev Alur, Rastislav Bod\u00edk, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2015. Syntax-guided synthesis. In Dependable Software Systems Engineering 2015."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Arjun Radhakrishna and Abhishek Udupa. 2017. Scaling enumerative program synthesis via divide and conquer. In Tools and Algorithms for the Construction and Analysis of Systems.  Rajeev Alur Arjun Radhakrishna and Abhishek Udupa. 2017. Scaling enumerative program synthesis via divide and conquer. In Tools and Algorithms for the Construction and Analysis of Systems.","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503275"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2018.00074"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Mike Barnett K. Rustan M. Leino and Wolfram Schulte. 2005. The Spec# Programming System: An Overview. In Construction and Analysis of Safe Secure and Interoperable Smart Devices.  Mike Barnett K. Rustan M. Leino and Wolfram Schulte. 2005. The Spec# Programming System: An Overview. In Construction and Analysis of Safe Secure and Interoperable Smart Devices.","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297069"},{"key":"e_1_2_1_10_1","volume-title":"Semantic Program Alignment for Equivalence Checking. In PLDI","author":"Churchill Berkeley","year":"2019","unstructured":"Berkeley Churchill , Oded Padon , Rahul Sharma , and Alex Aiken . 2019 . Semantic Program Alignment for Equivalence Checking. In PLDI 2019. Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken. 2019. Semantic Program Alignment for Equivalence Checking. In PLDI 2019."},{"key":"e_1_2_1_11_1","volume-title":"Automatic Inference of Necessary Preconditions","author":"Cousot Patrick","unstructured":"Patrick Cousot , Radhia Cousot , Manuel F\u00e4hndrich , and Francesco Logozzo . 2013. Automatic Inference of Necessary Preconditions . In Verification, Model Checking, and Abstract Interpretation, Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . isbn:978-3-642-35873-9 Patrick Cousot, Radhia Cousot, Manuel F\u00e4hndrich, and Francesco Logozzo. 2013. Automatic Inference of Necessary Preconditions. In Verification, Model Checking, and Abstract Interpretation, Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. isbn:978-3-642-35873-9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_14_1","volume-title":"FSE","author":"DeFreez Daniel","year":"2019","unstructured":"Daniel DeFreez , Haaken Martinson Baldwin , Cindy Rubio-Gonz\u00e1lez , and Aditya V. Thakur . 2019. Effective error-specification inference via domain-knowledge expansion . In FSE 2019 . Daniel DeFreez, Haaken Martinson Baldwin, Cindy Rubio-Gonz\u00e1lez, and Aditya V. Thakur. 2019. Effective error-specification inference via domain-knowledge expansion. In FSE 2019."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_2_1_16_1","unstructured":"Nii Dodoo Lin Li and Michael Ernst. 2003. Selecting Refining and Evaluating Predicates for Program Analysis.  Nii Dodoo Lin Li and Michael Ernst. 2003. Selecting Refining and Evaluating Predicates for Program Analysis."},{"key":"e_1_2_1_17_1","volume-title":"Dynamically Discovering Likely Program Invariants","author":"Ernst Michael D.","unstructured":"Michael D. Ernst . 2000. Dynamically Discovering Likely Program Invariants . University of Washington Department of Computer Science and Engineering. Seattle , Washington. Michael D. Ernst. 2000. Dynamically Discovering Likely Program Invariants. University of Washington Department of Computer Science and Engineering. Seattle, Washington."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302467"},{"key":"e_1_2_1_19_1","volume-title":"OOPSLA","author":"Ezudheen P.","year":"2018","unstructured":"P. Ezudheen , Daniel Neider , Deepak D\u2019Souza , Pranav Garg , and P. Madhusudan . 2018. Horn-ICE learning for synthesizing invariants and contracts . In OOPSLA 2018 . P. Ezudheen, Daniel Neider, Deepak D\u2019Souza, Pranav Garg, and P. Madhusudan. 2018. Horn-ICE learning for synthesizing invariants and contracts. In OOPSLA 2018."},{"key":"e_1_2_1_20_1","volume-title":"Static Verification for Code Contracts. In SAS","author":"F\u00e4hndrich Manuel","year":"2010","unstructured":"Manuel F\u00e4hndrich . 2010 . Static Verification for Code Contracts. In SAS 2010. Manuel F\u00e4hndrich. 2010. Static Verification for Code Contracts. In SAS 2010."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/367149.367170"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001464"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081713"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_27_1","volume-title":"Test Oracle Assessment and Improvement. In ISSTA","author":"Jahangirova Gunel","year":"2016","unstructured":"Gunel Jahangirova , David Clark , Mark Harman , and Paolo Tonella . 2016 . Test Oracle Assessment and Improvement. In ISSTA 2016. Gunel Jahangirova, David Clark, Mark Harman, and Paolo Tonella. 2016. Test Oracle Assessment and Improvement. In ISSTA 2016."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314634"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Gary T. Leavens Albert L. Baker and Clyde Ruby. 2006. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. SIGSOFT Softw. Eng. Notes.  Gary T. Leavens Albert L. Baker and Clyde Ruby. 2006. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. SIGSOFT Softw. Eng. Notes.","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_30_1","volume-title":"Object-Oriented Software Construction","author":"Meyer Bertrand","unstructured":"Bertrand Meyer . 1988. Object-Oriented Software Construction ( 1 st ed.). Prentice-Hall, Inc. , USA. isbn:0136290493 Bertrand Meyer. 1988. Object-Oriented Software Construction (1st ed.). Prentice-Hall, Inc., USA. isbn:0136290493","edition":"1"},{"key":"e_1_2_1_31_1","unstructured":"Thomas M. Mitchell. 1997. Machine Learning (1 ed.).  Thomas M. Mitchell. 1997. Machine Learning (1 ed.)."},{"key":"e_1_2_1_32_1","volume-title":"Frias","author":"Molina Facundo","year":"2021","unstructured":"Facundo Molina , Pablo Ponzio , Nazareno Aguirre , and Marcelo F . Frias . 2021 . EvoSpex: An Evolutionary Algorithm for Learning Postconditions . arxiv:2102.13569. Facundo Molina, Pablo Ponzio, Nazareno Aguirre, and Marcelo F. Frias. 2021. EvoSpex: An Evolutionary Algorithm for Learning Postconditions. arxiv:2102.13569."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0893-6080(95)00120-4"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_11"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428234"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428285"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297846.1297902"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227137"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572284"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Andrew Reynolds Haniel Barbosa Andres N\u00f6tzli Clark Barrett and Cesare Tinelli. 2019. cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. In Computer Aided Verification.  Andrew Reynolds Haniel Barbosa Andres N\u00f6tzli Clark Barrett and Cesare Tinelli. 2019. cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis. In Computer Aided Verification.","DOI":"10.1007\/978-3-030-25543-5_5"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568285"},{"key":"e_1_2_1_43_1","volume-title":"Understanding Z: A Specification Language and Its Formal Semantics","author":"Spivey J. M.","unstructured":"J. M. Spivey . 1988. Understanding Z: A Specification Language and Its Formal Semantics . Cambridge University Press , USA. isbn:0521334292 J. M. Spivey. 1988. Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, USA. isbn:0521334292"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409758"},{"key":"e_1_2_1_45_1","volume-title":"Pex: White Box Test Generation for .NET. In Tests and Proofs.","author":"Tillmann Nikolai","year":"2008","unstructured":"Nikolai Tillmann and Jonathan De Halleux . 2008 . Pex: White Box Test Generation for .NET. In Tests and Proofs. Nikolai Tillmann and Jonathan De Halleux. 2008. Pex: White Box Test Generation for .NET. In Tests and Proofs."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566212"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134427"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409716"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485481","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485481","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:39Z","timestamp":1750191519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485481"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":49,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485481"],"URL":"https:\/\/doi.org\/10.1145\/3485481","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}