Viktor Kuncak
Mikaël Mayer
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.
- Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-driven compositional symbolic execution. In Tools and Algorithms for the Construction and Analysis of Systems, 2008. Google Scholar
Digital Library
- Eugene Asarin, Oded Maler, and Amir Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems II, pages 1--20, 1995. Google ScholarCross Ref
- Utpal K. Banerjee. Dependence Analysis for Supercomputing. Kluwer Academic Publishers, Norwell, MA, USA, 1988. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Aaron R. Bradley and Zohar Manna. The Calculus of Computation. Springer, 2007.Google Scholar
- R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677--691, August 1986. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Cliff Stein. Introduction to Algorithms (Second Edition). MIT Press and McGraw-Hill, 2001. Google ScholarDigital Library
- 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.Google Scholar
- Robert K. Dewar. Programming by refinement, as exemplified by the SETL representation sublanguage. ACM TOPLAS, July 1979. Google ScholarDigital Library
- Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, Inc., 1976. Google ScholarDigital Library
- Burak Emir, Martin Odersky, and John Williams. Matching objects with patterns. In ECOOP, 2007. Google ScholarDigital Library
- Friedrich Eisenbrand and Gennady Shmonin. Parametric integer programming in fixed dimension. Mathematics of Operations Research, 33(4):839--850, 2008.Google ScholarCross Ref
- David Ford and George Havas. A new algorithm and refined bounds for extended gcd computation. In ANTS, pages 145--150, 1996. Google ScholarDigital Library
- Cormac Flanagan, K. Rustan M. Leino, Mark Lilibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking for Java. In PLDI, 2002. Google ScholarDigital Library
- Jeanne Ferrante and Charles W. Rackoff. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, 1979.Google Scholar
- S. Feferman and R. L. Vaught. The first order properties of products of algebraic systems. Fundamenta Mathematicae, 47:57--103, 1959.Google ScholarCross Ref
- Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast decision procedures. In CAV, pages 175--188, 2004.Google Scholar
- S. Ginsburg and E. Spanier. Bounded algol-like languages. Transactions of the American Mathematical Society, 113(2):333--368, 1964.Google ScholarCross Ref
- S. Ginsburg and E. Spanier. Semigroups, Presburger formulas and languages. Pacific Journal of Mathematics, 16(2):285--296, 1966.Google ScholarCross Ref
- Swen Jacobs. Hierarchic Decision Procedures for Verification. PhD thesis, Universität des Saarlandes, 2010.Google Scholar
- Barbara Jobstmann and Roderick Bloem. Optimizations for LTL synthesis. In FMCAD, 2006. Google ScholarDigital Library
- Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. (freely available), 1993. Google ScholarDigital Library
- Barbara Jobstmann, Stefan Galler, Martin Weiglhofer, and Roderick Bloem. Anzu: A tool for property synthesis. In CAV, volume 4590 of LNCS, 2007. Google ScholarDigital Library
- Joxan Jaffar and Michael J. Maher. Constraint logic programming: A survey. J. Log. Program., 19/20:503--581, 1994.Google ScholarCross Ref
- Felix Klaedtke. On the automata size for presburger arithmetic. Technical Report 186, Institute of Computer Science at Freiburg University, 2003.Google Scholar
- 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.Google Scholar
- Viktor Kuncak, Hai Huu Nguyen, and Martin Rinard. Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning, 2006. Google ScholarDigital Library
- Viktor Kuncak, Ruzica Piskac, Philippe Suter, and Thomas Wies. Building a calculus of data structures. In VMCAI, volume 5944 of LNCS, 2010. Google ScholarDigital Library
- Viktor Kuncak and Martin Rinard. Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In CADE-21, volume 4603 of LNCS, 2007. Google ScholarDigital Library
- Nils Klarlund and Michael I. Schwartzbach. Graph types. In POPL, Charleston, SC, 1993. Google ScholarDigital Library
- James H. Kukula and Thomas R. Shiple. Building circuits from relations. In CAV, 2000. Google ScholarDigital Library
- Scott McPeak and George C. Necula. Data structure specifications via local equality axioms. In CAV, pages 476--490, 2005. Google ScholarDigital Library
- Michał Moskal. Satisfiability Modulo Software. PhD thesis, University of Wrocław, 2009.Google Scholar
- Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- Zohar Manna and Richard J. Waldinger. Toward automatic program synthesis. Commun. ACM, 14(3):151--165, 1971. Google ScholarDigital Library
- Zohar Manna and Richard Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst., 2(1):90--121, 1980. Google ScholarDigital Library
- Tobias Nipkow. Linear quantifier elimination. In IJCAR, 2008. Google ScholarDigital Library
- Derek C. Oppen. Reasoning about recursively defined data structures. In POPL, pages 151--157, 1978. Google ScholarDigital Library
- Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008. Google ScholarDigital Library
- Ruzica Piskac and Viktor Kuncak. Decision procedures for multisets with cardinality constraints. In VMCAI, volume 4905 of LNCS, 2008. Google ScholarDigital Library
- Ruzica Piskac and Viktor Kuncak. Linear arithmetic with stars. In CAV, volume 5123 of LNCS, 2008. Google ScholarDigital Library
- Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. In VMCAI, 2006. Google ScholarDigital Library
- Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. In POPL, 1989. Google ScholarDigital Library
- Ruzica Piskac, Philippe Suter, and Viktor Kuncak. On decision procedures for ordered collections. Technical Report LARA-REPORT-2010-001, EPFL, 2010.Google Scholar
- William Pugh. A practical algorithm for exact array dependence analysis. Commun. ACM, 35(8):102--114, 1992. Google ScholarDigital Library
- Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, 1998. Google ScholarDigital Library
- Philippe Suter, Mirco Dotta, and Viktor Kuncak. Decision procedures for algebraic data types with abstractions. In POPL, 2010. Google ScholarDigital Library
- Don Syme, Adam Granicz, and Antonio Cisternino. Expert F#. Apress, 2007.Google Scholar
- Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. From program verification to program synthesis. In POPL, 2010. Google ScholarDigital Library
- Micha Sharir. Some observations concerning formal differentiation of set theoretic expressions. Transactions on Programming Languages and Systems, 4(2), April 1982. Google ScholarDigital Library
- Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodík, Vijay A. Saraswat, and Sanjit A. Seshia. Sketching stencils. In PLDI, 2007. Google ScholarDigital Library
- Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodík. Sketching concurrent data structures. In PLDI, 2008. Google ScholarDigital Library
- Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS, 2006. Google ScholarDigital Library
- R.C. Sekar, R. Ramesh, and I.V. Ramakrishnan. Adaptive pattern matching. SIAM Journal on Computing, 24:1207--1234, December 1995. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Martin T. Vechev, Eran Yahav, and Greta Yorsh. Inferring synchronization under limited observability. In TACAS, 2009. Google ScholarDigital Library
- Volker Weispfenning. Complexity and uniformity of elimination in presburger arithmetic. In Proc. International Symposium on Symbolic and Algebraic Computation, pages 48--53, 1997. Google ScholarDigital Library
- Thomas Wies, Ruzica Piskac, and Viktor Kuncak. Combining theories with shared set operations. In FroCoS: Frontiers in Combining Systems, 2009. Google ScholarDigital Library
- Kuat Yessenov, Ruzica Piskac, and Viktor Kuncak. Collections, cardinalities, and relations. In VMCAI, volume 5944 of LNCS, 2010. Google ScholarDigital Library
- Calogero G. Zarba. A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In 18th International Workshop on Unification, 2004.Google Scholar
- Calogero G. Zarba. Combining sets with cardinals. J. of Automated Reasoning, 34(1), 2005. Google ScholarDigital Library
- Karen Zee, Viktor Kuncak, and Martin Rinard. Full functional verification of linked data structures. In PLDI, 2008. Google ScholarDigital Library
Index Terms
- Complete functional synthesis
Recommendations
Complete functional synthesis
PLDI '10Synthesis 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 automataWe 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