Viktor Kuncak
Mikaël Mayer
Abstract
Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specifications. We propose to systematically generalize decision procedures into synthesis procedures, and use them to compile implicitly specified computations embedded inside functional and imperative programs. Synthesis procedures are predictable, because they are guaranteed to find code that satisfies the specification whenever such code exists. To illustrate our method, we derive synthesis procedures by extending quantifier elimination algorithms for integer arithmetic and set data structures. We then show that an implementation of such synthesis procedures can extend a compiler to support implicit value definitions and advanced pattern matching.
- Bradley, A.R., Manna, Z. The Calculus of Computation, Springer, Berlin, Germany, 2007.Google Scholar
Cross Ref
- Cohen, H. A Course in Computational Algebraic Number Theory. Springer, Berlin, Germany, 1993. Google ScholarCross Ref
- de Moura, L., Bjørner, N. Z3: An efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Inc., Upper Saddle River, NJ, 1976. Google ScholarDigital Library
- Ferrante, J., Rackoff, C.W. The Computational Complexity of Logical Theories, volume 718 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, Germany, 1979.Google ScholarCross Ref
- Flanagan, C., Leino, K.R.M., Lilibridge, M., Nelson, G., Saxe, J.B., Stata, R. Extended static checking for Java. In PLDI, 2002. Google ScholarDigital Library
- Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C. DPLL(T): Fast decision procedures. In CAV (2004), 175--188.Google Scholar
- Green, C.C. Application of theorem proving to problem solving. In IJCAI (1969), 219--240. Google ScholarDigital Library
- Hamza, J., Jobstmann, B., Kuncak, V. Synthesis for regular specifications over unbounded domains. In FMCAD, 2010. Google ScholarDigital Library
- Jaffar, J., Maher, M.J. Constraint logic programming: A survey. J. Log. Program, 19/20 (1994), 503--581.Google Scholar
- Joshi, R., Nelson, G., Zhou, Y. Denali: A practical algorithm for generating optimal code. ACM Trans. Program. Lang. Syst. 28 (2006), 967--989. Google ScholarDigital Library
- Kuncak, V., Mayer, M., Piskac, R., Suter, P. Complete functional synthesis. In PLDI, 2010. Google ScholarDigital Library
- Kuncak, V., Nguyen, H.H., Rinard, M. Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reason. 36, 3 (2006), 213--239. Google ScholarDigital Library
- Kuncak, V., Piskac, R., Suter, P. Ordered sets in the calculus of data structures. In CSL (2010), 34--48. Google ScholarDigital Library
- Manna, Z., Waldinger, R.J. Toward automatic program synthesis. Commun. ACM 14, 3 (1971), 151--165. Google ScholarDigital Library
- Odersky, M., Spoon, L., Venners, B. Programming in Scala: A Comprehensive Step-By-Step Guide. Artima Press, Mountain View, CA, 2008. Google ScholarDigital Library
- Oppen, D.C. Reasoning about recursively defined data structures. In POPL (1978), 151--157. Google ScholarDigital Library
- Piskac, R., Kuncak, V. Linear arithmetic with stars. In CAV, volume 5123 of LNCS, 2008. Google ScholarDigital Library
- Pnueli, A., Rosner, R. On the synthesis of a reactive module. In POPL, 1989. Google ScholarDigital Library
- Pugh, W. A practical algorithm for exact array dependence analysis. Commun. ACM 35, 8 (1992), 102--114. Google ScholarDigital Library
- Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A. Combinatorial sketching for finite programs. In ASPLOS, 2006. Google ScholarDigital Library
- Srivastava, S., Gulwani, S., Foster, J.S. From program verification to program synthesis. In POPL, 2010. Google ScholarDigital Library
- Suter, P., Dotta, M., Kuncak, V. Decision procedures for algebraic data types with abstractions. In POPL, 2010. Google ScholarDigital Library
- Zee, K., Kuncak, V., Rinard, M. Full functional verification of linked data structures. In PLDI, 2008. Google ScholarDigital Library
Index Terms
- Software synthesis procedures
Recommendations
Reductions for Synthesis Procedures
VMCAI 2013: Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 7737A synthesis procedure acts as a compiler for declarative specifications. It accepts a formula describing a relation between inputs and outputs, and generates a function implementing this relation. This paper presents the first synthesis procedures for 1 ...
Algorithmic Program Synthesis with Partial Programs and Decision Procedures
SAS '09: Proceedings of the 16th International Symposium on Static AnalysisProgram synthesizer can derive programs that are efficient, even surprising, but it must be first "programmed" with human insights about the domain and its implementation tricks. In deductive synthesis, the insights are captured by domain theories, ...
Comments