research-article

Complete functional synthesis

Authors:

Philippe SuterAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 6

Pages 316 - 329

https://doi.org/10.1145/1809028.1806632

Published: 05 June 2010 Publication History

Abstract

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way - they should succeed for a well-defined class of specifications. They should also support unbounded data types such as numbers and data structures. We propose to generalize decision procedures into predictable and complete synthesis procedures. Such procedures are guaranteed to find code that satisfies the specification if such code exists. Moreover, we identify conditions under which synthesis will statically decide whether the solution is guaranteed to exist, and whether it is unique. We demonstrate our approach by starting from decision procedures for linear arithmetic and data structures and transforming them into synthesis procedures. We establish results on the size and the efficiency of the synthesized code. We show that such procedures are useful as a language extension with implicit value definitions, and we show how to extend a compiler to support such definitions. Our constructs provide the benefits of synthesis to programmers, without requiring them to learn new concepts or give up a deterministic execution model.

References

[1]

Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-driven compositional symbolic execution. In Tools and Algorithms for the Construction and Analysis of Systems, 2008.

Digital Library

[2]

Eugene Asarin, Oded Maler, and Amir Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems II, pages 1--20, 1995.

[3]

Utpal K. Banerjee. Dependence Analysis for Supercomputing. Kluwer Academic Publishers, Norwell, MA, USA, 1988.

Digital Library

[4]

Bernard Boigelot, Sébastien Jodogne, and Pierre Wolper. An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Logic, 6(3):614--633, 2005.

Digital Library

[5]

Aaron R. Bradley and Zohar Manna. The Calculus of Computation. Springer, 2007.

[6]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, August 1986.

Digital Library

[7]

Clark Barrett, Igor Shikanian, and Cesare Tinelli. An abstract decision procedure for satisfiability in the theory of recursive data types. Electronic Notes in Theoretical Computer Science, 174(8):23--37, 2007.

Digital Library

[8]

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliff Stein. Introduction to Algorithms (Second Edition). MIT Press and McGraw-Hill, 2001.

Digital Library

[9]

D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 7, pages 91--100. Edinburgh University Press, 1972.

[10]

Robert K. Dewar. Programming by refinement, as exemplified by the SETL representation sublanguage. ACM TOPLAS, July 1979.

Digital Library

[11]

Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Inc., 1976.

Digital Library

[12]

Burak Emir, Martin Odersky, and John Williams. Matching objects with patterns. In ECOOP, 2007.

Digital Library

[13]

Friedrich Eisenbrand and Gennady Shmonin. Parametric integer programming in fixed dimension. Mathematics of Operations Research, 33(4):839--850, 2008.

[14]

David Ford and George Havas. A new algorithm and refined bounds for extended gcd computation. In ANTS, pages 145--150, 1996.

Digital Library

[15]

Cormac Flanagan, K. Rustan M. Leino, Mark Lilibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking for Java. In PLDI, 2002.

Digital Library

[16]

Jeanne Ferrante and Charles W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[17]

S. Feferman and R. L. Vaught. The first order properties of products of algebraic systems. Fundamenta Mathematicae, 47:57--103, 1959.

[18]

Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In CAV, pages 175--188, 2004.

[19]

S. Ginsburg and E. Spanier. Bounded algol-like languages. Transactions of the American Mathematical Society, 113(2):333--368, 1964.

[20]

S. Ginsburg and E. Spanier. Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2):285--296, 1966.

[21]

Swen Jacobs. Hierarchic Decision Procedures for Verification. PhD thesis, Universität des Saarlandes, 2010.

[22]

Barbara Jobstmann and Roderick Bloem. Optimizations for LTL synthesis. In FMCAD, 2006.

Digital Library

[23]

Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. (freely available), 1993.

Digital Library

[24]

Barbara Jobstmann, Stefan Galler, Martin Weiglhofer, and Roderick Bloem. Anzu: A tool for property synthesis. In CAV, volume 4590 of LNCS, 2007.

Digital Library

[25]

Joxan Jaffar and Michael J. Maher. Constraint logic programming: A survey. J. Log. Program., 19/20:503--581, 1994.

[26]

Felix Klaedtke. On the automata size for presburger arithmetic. Technical Report 186, Institute of Computer Science at Freiburg University, 2003.

[27]

Nils Klarlund and Anders Møller. MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science, University of Aarhus, January 2001.

[28]

Viktor Kuncak, Hai Huu Nguyen, and Martin Rinard. Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning, 2006.

Digital Library

[29]

Viktor Kuncak, Ruzica Piskac, Philippe Suter, and Thomas Wies. Building a calculus of data structures. In VMCAI, volume 5944 of LNCS, 2010.

Digital Library

[30]

Viktor Kuncak and Martin Rinard. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In CADE-21, volume 4603 of LNCS, 2007.

Digital Library

[31]

Nils Klarlund and Michael I. Schwartzbach. Graph types. In POPL, Charleston, SC, 1993.

Digital Library

[32]

James H. Kukula and Thomas R. Shiple. Building circuits from relations. In CAV, 2000.

Digital Library

[33]

Scott McPeak and George C. Necula. Data structure specifications via local equality axioms. In CAV, pages 476--490, 2005.

Digital Library

[34]

Michał Moskal. Satisfiability Modulo Software. PhD thesis, University of Wrocław, 2009.

[35]

Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.

Digital Library

[36]

Zohar Manna and Richard J. Waldinger. Toward automatic program synthesis. Commun. ACM, 14(3):151--165, 1971.

Digital Library

[37]

Zohar Manna and Richard Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst., 2(1):90--121, 1980.

Digital Library

[38]

Tobias Nipkow. Linear quantifier elimination. In IJCAR, 2008.

Digital Library

[39]

Derek C. Oppen. Reasoning about recursively defined data structures. In POPL, pages 151--157, 1978.

Digital Library

[40]

Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008.

Digital Library

[41]

Ruzica Piskac and Viktor Kuncak. Decision procedures for multisets with cardinality constraints. In VMCAI, volume 4905 of LNCS, 2008.

Digital Library

[42]

Ruzica Piskac and Viktor Kuncak. Linear arithmetic with stars. In CAV, volume 5123 of LNCS, 2008.

Digital Library

[43]

Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. In VMCAI, 2006.

Digital Library

[44]

Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, 1989.

Digital Library

[45]

Ruzica Piskac, Philippe Suter, and Viktor Kuncak. On decision procedures for ordered collections. Technical Report LARA-REPORT-2010-001, EPFL, 2010.

[46]

William Pugh. A practical algorithm for exact array dependence analysis. Commun. ACM, 35(8):102--114, 1992.

Digital Library

[47]

Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, 1998.

Digital Library

[48]

Philippe Suter, Mirco Dotta, and Viktor Kuncak. Decision procedures for algebraic data types with abstractions. In POPL, 2010.

Digital Library

[49]

Don Syme, Adam Granicz, and Antonio Cisternino. Expert F#. Apress, 2007.

[50]

Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. From program verification to program synthesis. In POPL, 2010.

Digital Library

[51]

Micha Sharir. Some observations concerning formal differentiation of set theoretic expressions. Transactions on Programming Languages and Systems, 4(2), April 1982.

Digital Library

[52]

Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodík, Vijay A. Saraswat, and Sanjit A. Seshia. Sketching stencils. In PLDI, 2007.

Digital Library

[53]

Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodík. Sketching concurrent data structures. In PLDI, 2008.

Digital Library

[54]

Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006.

Digital Library

[55]

R.C. Sekar, R. Ramesh, and I.V. Ramakrishnan. Adaptive pattern matching. SIAM Journal on Computing, 24:1207--1234, December 1995.

Digital Library

[56]

Martin T. Vechev, Eran Yahav, David F. Bacon, and Noam Rinetzky. Cgcexplorer: a semi-automated search procedure for provably correct concurrent collectors. In PLDI, pages 456--467, 2007.

Digital Library

[57]

Martin T. Vechev, Eran Yahav, and Greta Yorsh. Inferring synchronization under limited observability. In TACAS, 2009.

Digital Library

[58]

Volker Weispfenning. Complexity and uniformity of elimination in presburger arithmetic. In Proc. International Symposium on Symbolic and Algebraic Computation, pages 48--53, 1997.

Digital Library

[59]

Thomas Wies, Ruzica Piskac, and Viktor Kuncak. Combining theories with shared set operations. In FroCoS: Frontiers in Combining Systems, 2009.

Digital Library

[60]

Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak. Collections, cardinalities, and relations. In VMCAI, volume 5944 of LNCS, 2010.

Digital Library

[61]

Calogero G. Zarba. A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In 18th International Workshop on Unification, 2004.

[62]

Calogero G. Zarba. Combining sets with cardinals. J. of Automated Reasoning, 34(1), 2005.

Digital Library

[63]

Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In PLDI, 2008.

Digital Library

Cited By

Akshay SChakraborty SShah S(2023)Tractable representations for Boolean functional synthesisAnnals of Mathematics and Artificial Intelligence10.1007/s10472-023-09907-592:5(1051-1096)Online publication date: 5-Dec-2023
https://dl.acm.org/doi/10.1007/s10472-023-09907-5
Akshay SChakraborty SJain S(2023)Counterexample Guided Knowledge Compilation for Boolean Functional SynthesisComputer Aided Verification10.1007/978-3-031-37706-8_19(367-389)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_19
Akshay SChakraborty S(2022)Synthesizing Skolem Functions: A View from Theory and PracticeHandbook of Logical Thought in India10.1007/978-81-322-2577-5_51(1187-1222)Online publication date: 5-Nov-2022
https://doi.org/10.1007/978-81-322-2577-5_51
Show More Cited By

Index Terms

Complete functional synthesis
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

Complete functional synthesis
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algorithms should behave in a predictable way - they should succeed for a well-...
Deciding Boolean Algebra with Presburger Arithmetic

We describe an algorithm for deciding the first-order multisorted theory BAPA, which combines Boolean algebras of sets of uninterpreted elements (BA) and Presburger arithmetic operations (PA). BAPA can express the relationship between integer variables ...
Past pushdown timed automata and safety verification
Implementation and application automata

We consider past pushdown timed automata that are discrete pushdown timed automata with past formulas as enabling conditions. Using past formulas allows a past pushdown timed automaton to access the past values of the finite state variables in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 45, Issue 6

PLDI '10

June 2010

496 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1809028

Issue’s Table of Contents

PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2010
514 pages
ISBN:9781450300193
DOI:10.1145/1806596
General Chair:
Ben Zorn
Microsoft Research
,
Program Chair:
Alex Aiken
Stanford University

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 June 2010

Published in SIGPLAN Volume 45, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

140
Total Citations
View Citations
788
Total Downloads

Downloads (Last 12 months)40
Downloads (Last 6 weeks)10

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Akshay SChakraborty SShah S(2023)Tractable representations for Boolean functional synthesisAnnals of Mathematics and Artificial Intelligence10.1007/s10472-023-09907-592:5(1051-1096)Online publication date: 5-Dec-2023
https://dl.acm.org/doi/10.1007/s10472-023-09907-5
Akshay SChakraborty SJain S(2023)Counterexample Guided Knowledge Compilation for Boolean Functional SynthesisComputer Aided Verification10.1007/978-3-031-37706-8_19(367-389)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_19
Akshay SChakraborty S(2022)Synthesizing Skolem Functions: A View from Theory and PracticeHandbook of Logical Thought in India10.1007/978-81-322-2577-5_51(1187-1222)Online publication date: 5-Nov-2022
https://doi.org/10.1007/978-81-322-2577-5_51
Akshay SChakraborty S(2022)Synthesizing Skolem Functions: A View from Theory and PracticeHandbook of Logical Thought in India10.1007/978-81-322-1812-8_51-1(1-36)Online publication date: 1-Jul-2022
https://doi.org/10.1007/978-81-322-1812-8_51-1
Itzhaky SPeleg HPolikarpova NRowe RSergey IFreund SYahav E(2021)Cyclic program synthesisProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454087(944-959)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454087
Shah PBansal AAkshay SChakraborty SGorla D(2021)A normal form characterization for efficient boolean skolem function synthesisProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470741(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470741
Akshay SChakraborty SGoel SKulal SShah S(2021)Boolean functional synthesis: hardness and practical algorithmsFormal Methods in System Design10.1007/s10703-020-00352-257:1(53-86)Online publication date: 1-Jul-2021
https://dl.acm.org/doi/10.1007/s10703-020-00352-2
Akshay SArora JChakraborty SKrishna SRaghunathan DShah S(2019)Knowledge Compilation for Boolean Functional Synthesis2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894266(161-169)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894266
Finkbeiner BKlein FPiskac RSantolucito MEisenberg R(2019)Synthesizing functional reactive programsProceedings of the 12th ACM SIGPLAN International Symposium on Haskell10.1145/3331545.3342601(162-175)Online publication date: 8-Aug-2019
https://dl.acm.org/doi/10.1145/3331545.3342601
Akshay SChakraborty SGoel SKulal SShah S(2018)What’s Hard About Boolean Functional Synthesis?Computer Aided Verification10.1007/978-3-319-96145-3_14(251-269)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96145-3_14
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents