×

zbMATH — the first resource for mathematics

Refutation-based synthesis in SMT. (English) Zbl 1427.68051
Summary: We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifications are single-invocation properties, for which we present a dedicated algorithm. To support syntax restrictions on generated solutions, our approach can transform a solution found without restrictions into the desired syntactic form. As an alternative, we show how to use evaluation function axioms to embed syntactic restrictions into constraints over algebraic datatypes, and then use an algebraic datatype decision procedure to drive synthesis. Our experimental evaluation on syntax-guided synthesis benchmarks shows that our implementation in the CVC4 SMT solver is competitive with state-of-the-art tools for synthesis.
MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Solving difficult sat instances in the presence of symmetry. In: Proceedings of the 39th annual design automation conference. ACM, pp 731-736
[2] Alur R, Bodik R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2014) Syntax-guided synthesis. In: Marktoberdrof NATO proceedings (to appear). http://sygus.seas.upenn.edu/files/sygus_extended.pdf, retrieved 2015-02-06
[3] Alur R, Bodík R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD. IEEE, pp 1-17
[4] Alur, Rajeev; Martin, Milo; Raghothaman, Mukund; Stergiou, Christos; Tripakis, Stavros; Udupa, Abhishek, Synthesizing Finite-State Protocols from Scenarios and Requirements, Hardware and Software: Verification and Testing, 75-91 (2014), Cham: Springer International Publishing, Cham
[5] Barrett C, Conway C, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: Proceedings of CAV’11, LNCS, vol 6806. Springer, pp 171-177
[6] Barrett, C.; Deters, M.; De Moura, Lm; Oliveras, A.; Stump, A., 6 years of SMT-COMP, JAR, 50, 3, 243-277 (2013)
[7] Barrett, C.; Shikanian, I.; Tinelli, C., An abstract decision procedure for satisfiability in the theory of inductive data types, J Satisf Boolean Model Comput, 3, 21-46 (2007) · Zbl 1129.68022
[8] Bjørner, Nikolaj, Linear Quantifier Elimination as an Abstract Decision Procedure, Automated Reasoning, 316-330 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1291.68325
[9] Bloem, R.; Jobstmann, B.; Piterman, N.; Pnueli, A.; Sa’Ar, Y., Synthesis of reactive(1) designs, J Comput Syst Sci, 78, 3, 911-938 (2012) · Zbl 1247.68050
[10] Constable, Rl; Allen, Sf; Bromley, M.; Cleaveland, R.; Cremer, Jf; Harper, Rw; Howe, Dj; Knoblock, Tb; Mendler, Np; Panangaden, P.; Sasaki, Jt; Smith, Sf, Implementing mathematics with the Nuprl proof development system (1986), Englewood Cliffs: Prentice Hall, Englewood Cliffs
[11] Cousot, Patrick, Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming, Lecture Notes in Computer Science, 1-24 (2005), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1111.68503
[12] Déharbe D, Fontaine P, Merz S, Paleo BW (2011) Exploiting symmetry in SMT problems. In: Automated deduction—CADE-23. Springer, pp 222-236 · Zbl 1341.68187
[13] Detlefs D, Nelson G, Saxe, JB (2003) Simplify: a theorem prover for program checking. Technical report. J ACM · Zbl 1323.68462
[14] Dutertre B (2015) Solving exists/forall problems with yices. In: Workshop on satisfiability modulo theories
[15] Finkbeiner, B.; Schewe, S., Bounded synthesis, STTT, 15, 5-6, 519-539 (2013)
[16] Ge Y, Barrett C, Tinelli C (2007) Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning F (ed) CADE, LNCS, vol 4603. Springer, pp 167-182. doi:10.1007/978-3-540-73595-3_12 · Zbl 1213.68376
[17] Ge, Yeting; De Moura, Leonardo, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification, 306-320 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1242.68280
[18] Green, Cc; Walker, De; Norton, Lm, Application of theorem proving to problem solving, IJCAI, 219-240 (1969), Los Altos: William Kaufmann, Los Altos
[19] Jacobs, S.; Kuncak, V., Towards complete reasoning about axiomatic specifications, Verification, model checking, and abstract interpretation, 278-293 (2011), Berlin: Springer, Berlin · Zbl 1317.68117
[20] Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund, Solving QBF with Counterexample Guided Refinement, Theory and Applications of Satisfiability Testing - SAT 2012, 114-128 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1273.68178
[21] Janota M, Silva JPM (2011) Abstraction-based algorithm for 2qbf. In: Theory and applications of satisfiability testing—SAT 2011—14th international conference, SAT 2011, Proceedings, pp 230-244, Ann Arbor, MI, USA, 19-22 June 2011 · Zbl 1330.68115
[22] Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Kramer J, Bishop J, Devanbu PT, Uchitel S (eds) ICSE. ACM, pp 215-224. doi:10.1145/1806799.1806833
[23] Kneuss, Etienne; Koukoutos, Manos; Kuncak, Viktor, Deductive Program Repair, Computer Aided Verification, 217-233 (2015), Cham: Springer International Publishing, Cham
[24] Kneuss E, Kuraj I, Kuncak V, Suter P (2013) Synthesis modulo recursive functions. In: Hosking AL, Eugster PT, Lopes CV(eds) OOPSLA. ACM, pp 407-426. doi:10.1145/2509136.2509555
[25] Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification. Springer · Zbl 1358.68072
[26] Kuncak V, Mayer M, Piskac R, Suter P (2010)Complete functional synthesis. In: Zorn BG, Aiken A (eds) PLDI, pp 316-329. ACM. doi:10.1145/1806596.1806632
[27] Kuncak, V.; Mayer, M.; Piskac, R.; Suter, P., Software synthesis procedures, CACM, 55, 2, 103-111 (2012)
[28] Kuncak, V.; Mayer, M.; Piskac, R.; Suter, P., Functional synthesis for linear arithmetic and sets, STTT, 15, 5-6, 455-474 (2013)
[29] Madhavan, Ravichandhran; Kuncak, Viktor, Symbolic Resource Bound Inference for Functional Programs, Computer Aided Verification, 762-778 (2014), Cham: Springer International Publishing, Cham
[30] Manna, Z.; Waldinger, Rj, A deductive approach to program synthesis, TOPLAS, 2, 1, 90-121 (1980) · Zbl 0468.68009
[31] Monniaux, David, Quantifier Elimination by Lazy Model Enumeration, Computer Aided Verification, 585-599 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[32] De Moura, Leonardo; Bjørner, Nikolaj, Efficient E-Matching for SMT Solvers, Automated Deduction - CADE-21, 183-198 (2007), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1213.68578
[33] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164
[34] Perelman D, Gulwani S, Grossman D, Provost P (2010) Test-driven synthesis. In: O’Boyle MFP, Pingali K (eds) PLDI. ACM, p 43. doi:10.1145/2594291.2594297
[35] Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Conference record of the sixteenth annual ACM symposium on principles of programming languages, pp 179-190, Austin, TX, USA, 11-13 Jan 1989. doi:10.1145/75277.75293 · Zbl 0686.68015
[36] Presburger M (1929) Über die Vollständigkeit eines gewissen Systems der Aritmethik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier Congrès des Mathématiciens des Pays slaves, Warsawa, pp 92-101
[37] Raghothaman M., Udupa A (2014) Language to specify syntax-guided synthesis problems. CoRR arXiv:1405.5590
[38] Reynolds A, Deters M, Kuncak V, Tinelli C, Barrett CW (2015) Counterexample-guided quantifier instantiation for synthesis in SMT. In: Computer aided verification—27th international conference, CAV 2015, Proceedings, Part II, pp 198-216, San Francisco, CA, USA, 18-24 July 2015 · Zbl 1381.68059
[39] Reynolds A, King T, Kuncak V (2015) An instantiation-based approach for solving quantified linear arithmetic. CoRR arXiv:1510.02642 · Zbl 1377.68138
[40] Reynolds, Andrew; Tinelli, Cesare; Goel, Amit; Krstić, Sava; Deters, Morgan; Barrett, Clark, Quantifier Instantiation Techniques for Finite Model Finding in SMT, Automated Deduction - CADE-24, 377-391 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1381.68275
[41] Reynolds A, Tinelli C, Moura LD (2014) Finding conflicting instances of quantified formulas in SMT. In: Formal methods in computer-aided design (FMCAD)
[42] Ryzhyk L, Walker A, Keys J, Legg A, Raghunath A, Stumm M, Vij M (2014) User-guided device driver synthesis. In: Flinn J, Levy H (eds) OSDI. USENIX Association, pp 661-676
[43] Saha, Shambwaditya; Garg, Pranav; Madhusudan, P., Alchemist: Learning Guarded Affine Functions, Computer Aided Verification, 440-446 (2015), Cham: Springer International Publishing, Cham
[44] Schkufza, E.; Sharma, R.; Aiken, A., Stochastic superoptimization, SIGPLAN Not, 48, 4, 305-316 (2013)
[45] Solar-Lezama, A., Program sketching, STTT, 15, 5-6, 475-495 (2013)
[46] Solar-Lezama A, Tancau L, Bodík R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: Shen JP, Martonosi M (eds) ASPLOS. ACM, pp 404-415. doi:10.1145/1168857.1168907
[47] Srivastava, S.; Gulwani, S.; Foster, Js, Template-based program verification and program synthesis, STTT, 15, 5-6, 497-518 (2013)
[48] Stump A, Sutcliffe G, Tinelli C (2014) Starexec: a cross-community infrastructure for logic solving. In: Proceedings of the 7th international joint conference on automated reasoning, Lecture notes in artificial intelligence. Springer
[49] Svenningsson, Josef; Axelsson, Emil, Combining Deep and Shallow Embedding for EDSL, Lecture Notes in Computer Science, 21-36 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[50] Tiwari A, Gascón A, Dutertre B (2015) Program synthesis using dual interpretation. In: Automated deduction—CADE-25—25th international conference on automated deduction, Proceedings, Berlin, Germany, 1-7 Aug 2015, pp 482-497 · Zbl 06515527
[51] Udupa A, Raghavan A, Deshmukh JV, Mador-Haim S, Martin MM, Alur R (2013) Transit: specifying protocols with concolic snippets. In: PLDI. ACM, pp 287-296. doi:10.1145/2491956.2462174
[52] Wildmoser, Martin; Nipkow, Tobias, Certifying Machine Code Safety: Shallow Versus Deep Embedding, Lecture Notes in Computer Science, 305-320 (2004), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1099.68545
[53] Wintersteiger, Cm; Hamadi, Y.; De Moura, L., Efficiently solving quantified bit-vector formulas, Form Methods Syst Des, 42, 1, 3-23 (2013) · Zbl 1284.03212
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.