Cited By
View all- Campbell EHojjat HFoster N(2024)Computing Precise Control Interface SpecificationsProceedings of the ACM on Programming Languages10.1145/36897438:OOPSLA2(905-934)Online publication date: 8-Oct-2024
Synthesizing Specifications
Article No.: 285, Pages 1787 - 1816
Abstract
Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: i) a query posed about a set of function definitions, and ii) a domain-specific language L in which the extracted property is to be expressed (we call properties in the language L-properties). Each of the property is a best L-property for the query: there is no other L-property that is strictly more precise. Furthermore, the set of synthesized L-properties is exhaustive: no more L-properties can be added to it to make the conjunction more precise. We implemented our method in a tool, Spyro. The ability to modify both the query and L provides a Spyro user with ways to customize the kind of specification to be synthesized. We use this ability to show that Spyro can be used in a variety of applications, such as mining program specifications, performing abstract-domain operations, and synthesizing algebraic properties of program modules.
References
[1]
Rajeev Alur, Dana Fisman, Saswat Padhi, Rishabh Singh, and Abhishek Udupa. 2019. SyGuS-Comp 2018: Results and Analysis. https://doi.org/10.48550/ARXIV.1904.07146
[2]
Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, and Tao Xie. 2021. Synthesizing contracts correct modulo a test generator. Proc. ACM Program. Lang., 5, OOPSLA (2021), 1–27. https://doi.org/10.1145/3485481
[3]
Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. 2008. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program., 72, 1-2 (2008), 3–21. https://doi.org/10.1016/j.scico.2007.08.001
[4]
Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Dana Fisman and Grigore Rosu (Eds.) (Lecture Notes in Computer Science, Vol. 13243). Springer, 415–442. https://doi.org/10.1007/978-3-030-99524-9_24
[5]
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, SaiDeep Tetali, and Aditya V. Thakur. 2010. Proofs from Tests. IEEE Trans. Software Eng., 36, 4 (2010), 495–508. https://doi.org/10.1109/TSE.2010.49
[6]
Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC. 643–659. isbn:978-1-931971-40-9 https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/blazytko
[7]
Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238–252. https://doi.org/10.1145/512950.512973
[8]
Patrick Cousot and Radhia Cousot. 1978. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Descriptions of Programming Concepts. North-Holland.
[9]
Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, Alfred V. Aho, Stephen N. Zilles, and Thomas G. Szymanski (Eds.). ACM Press, 84–96. https://doi.org/10.1145/512760.512770
[10]
Loris D’Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin C. Pierce. 2013. Sensitivity analysis using type-based constraints. In Proceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages, FPCDSL@ICFP 2013, Boston, Massachusetts, USA, September 22, 2013, Richard Lazarus, Assaf J. Kfoury, and Jacob Beal (Eds.). ACM, 43–50. https://doi.org/10.1145/2505351.2505353
[11]
Isil Dillig, Thomas Dillig, and Alex Aiken. 2012. Automated error diagnosis using abductive inference. ACM SIGPLAN Notices, 47, 6 (2012), 181–192.
[12]
Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin. 2001. Dynamically Discovering Likely Program Invariants to Support Program Evolution. IEEE Trans. Software Eng., 27, 2 (2001), 99–123. https://doi.org/10.1109/32.908957
[13]
Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69, 1-3 (2007), 35–45. https://doi.org/10.1016/j.scico.2007.01.015
[14]
Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. 2014. ICE: A Robust Framework for Learning Invariants. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Armin Biere and Roderick Bloem (Eds.) (Lecture Notes in Computer Science, Vol. 8559). Springer, 69–87. https://doi.org/10.1007/978-3-319-08867-9_5
[15]
Denis Gopan and Thomas W. Reps. 2007. Low-Level Library Analysis and Summarization. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, Werner Damm and Holger Hermanns (Eds.) (Lecture Notes in Computer Science, Vol. 4590). Springer, 68–81. https://doi.org/10.1007/978-3-540-73368-3_10
[16]
Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In SAS.
[17]
Qinheping Hu, John Cyphert, Loris D’Antoni, and Thomas W. Reps. 2020. Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 1128–1142. https://doi.org/10.1145/3385412.3385979
[18]
Shachar Itzhaky. 2014. Automatic Reasoning for Pointer Programs Using Decidable Logics. Ph. D. Dissertation. Tel Aviv University.
[19]
Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D’Antoni, Thomas W. Reps, and Subhajit Roy. 2022. Synthesizing Abstract Transformers. Proc. ACM Program. Lang., https://doi.org/10.1145/3563334
[20]
Daniela Kaufmann, Paul Beame, Armin Biere, and Jakob Nordstrom. 2022. Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. In Proceedings of the 2022 Conference on Design, Automation Test in Europe (DATE ’22). European Design and Automation Association, Leuven, BEL. 1431–1436. isbn:9783981926361
[21]
Jinwoo Kim. 2022. Messy-Release. https://github.com/kjw227/Messy-Release
[22]
Jinwoo Kim, Qinheping Hu, Loris D’Antoni, and Thomas W. Reps. 2021. Semantics-guided synthesis. Proc. ACM Program. Lang., 5, POPL (2021), 1–32. https://doi.org/10.1145/3434311
[23]
K. Rustan M. Leino and Valentin Wüstholz. 2014. The Dafny Integrated Development Environment. In Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014, Catherine Dubois, Dimitra Giannakopoulou, and Dominique Méry (Eds.) (EPTCS, Vol. 149). 3–15. https://doi.org/10.4204/EPTCS.149.2
[24]
2017. Mining Software Specifications: Methodologies and Applications, David Lo, Siau-Cheng Khoo, Jiawei Han, and Chao Liu (Eds.). Chapman & Hall.
[25]
Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang Qiu, Jeffrey S. Foster, and Armando Solar-Lezama. 2019. Program Synthesis with Algebraic Library Specifications. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 132, Oct., 25 pages. https://doi.org/10.1145/3360558
[26]
Anders Miltner, Saswat Padhi, Todd Millstein, and David Walker. 2020. Data-Driven Inference of Representation Invariants. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA. 1–15. isbn:9781450376136 https://doi.org/10.1145/3385412.3385967
[27]
Tom M. Mitchell. 1997. Machine Learning. McGraw-Hill.
[28]
Or Ozeri, Oded Padon, Noam Rinetzky, and Mooly Sagiv. 2017. Conjunctive Abstract Interpretation Using Paramodulation. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Ahmed Bouajjani and David Monniaux (Eds.) (Lecture Notes in Computer Science, Vol. 10145). Springer, 442–461. https://doi.org/10.1007/978-3-319-52234-0_24
[29]
Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-driven precondition inference with learned features. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery D. Berger (Eds.). ACM, 42–56. https://doi.org/10.1145/2908080.2908099
[30]
Oded Padon. 2018. Deductive Verification of Distributed Protocols in First-Order Logic. Ph. D. Dissertation. Tel Aviv University.
[31]
Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken. 2022. Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang., 6, POPL (2022), 1–29. https://doi.org/10.1145/3498712
[32]
Kanghee Park, Loris D’Antoni, and Thomas Reps. 2023. Synthesizing Specifications. arxiv:2301.11117.
[33]
Kanghee Park, Loris D’Antoni, and Thomas Reps. 2023. Synthesizing Specifications. https://doi.org/10.5281/zenodo.8327699
[34]
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. ACM SIGPLAN Notices, 51, 6 (2016), 522–538.
[35]
Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. 252–266. https://doi.org/10.1007/978-3-540-24622-0_21
[36]
Thomas W. Reps and Aditya V. Thakur. 2016. Automating Abstract Interpretation. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 9583). Springer, 3–40. https://doi.org/10.1007/978-3-662-49122-5_1
[37]
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, 55–74. https://doi.org/10.1109/LICS.2002.1029817
[38]
Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM, 159–169. https://doi.org/10.1145/1375581.1375602
[39]
Micha Sharir and Amir Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall.
[40]
Nicholas Smallbone, Moa Johansson, Koen Claessen, and Maximilian Algehed. 2017. Quick specifications for the busy programmer. Journal of Functional Programming, 27 (2017), e18.
[41]
Armando Solar-Lezama. 2013. Program sketching. Int. J. Softw. Tools Technol. Transf., 15, 5-6 (2013), 475–495. https://doi.org/10.1007/s10009-012-0249-7
[42]
Aditya V. Thakur, Matt Elder, and Thomas W. Reps. 2012. Bilateral Algorithms for Symbolic Abstraction. In Static Analysis - 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings. 111–128. https://doi.org/10.1007/978-3-642-33125-1_10
[43]
Aditya V. Thakur and Thomas W. Reps. 2012. A Method for Symbolic Computation of Abstract Operations. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. 174–192. https://doi.org/10.1007/978-3-642-31424-7_17
[44]
Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming. 269–282.
[45]
Yu-Xiang Wang, Jing Lei, and Stephen E. Fienberg. 2016. Learning with Differential Privacy: Stability, Learnability and the Sufficiency and Necessity of ERM Principle. J. Mach. Learn. Res., 17, 1 (2016), jan, 6353–6392. issn:1532-4435
[46]
Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang. 2021. Program analysis via efficient symbolic abstraction. Proc. ACM Program. Lang., 5, OOPSLA (2021), 1–32. https://doi.org/10.1145/3485495
[47]
Zhe Zhou, Robert Dickerson, Benjamin Delaware, and Suresh Jagannathan. 2021. Data-driven abductive inference of library specifications. Proc. ACM Program. Lang., 5, OOPSLA (2021), 1–29. https://doi.org/10.1145/3485493
[48]
He Zhu, Stephen Magill, and Suresh Jagannathan. 2018. A data-driven CHC solver. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 707–721. https://doi.org/10.1145/3192366.3192416
Index Terms
- Synthesizing Specifications
Recommendations
Synthesizing Formal Semantics from Executable Interpreters
Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics for the language. Because writing a formal semantics can be a daunting ...
Synthesizing fault-tolerant programs from deontic logic specifications
ASE '13: Proceedings of the 28th IEEE/ACM International Conference on Automated Software EngineeringWe study the problem of synthesizing fault-tolerant components from specifications, i.e., the problem of automatically constructing a fault-tolerant component implementation from a logical specification of the component, and the system's required level ...
Synthesizing Imperative Code from Answer Set Programming Specifications
Logic-Based Program Synthesis and TransformationAbstractWe consider the problem of obtaining an implementation of an algorithm from its specification. We assume that these specifications are written in answer set programming (ASP). ASP is an ideal formalism for writing specifications due to its highly ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
2250 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 October 2023
Published in PACMPL Volume 7, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 467Total Downloads
- Downloads (Last 12 months)393
- Downloads (Last 6 weeks)70
Reflects downloads up to 10 Dec 2024
Other Metrics
Citations
Cited By
View all- Campbell EHojjat HFoster N(2024)Computing Precise Control Interface SpecificationsProceedings of the ACM on Programming Languages10.1145/36897438:OOPSLA2(905-934)Online publication date: 8-Oct-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in