[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Refutation-based synthesis in SMT

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

Notes

  1. That is, every \(\varSigma \)-interpretation isomorphic to an interpretation in \({\mathbf {I}}\) is also in \({\mathbf {I}}\).

  2. For \(T_1 \cup T_2\) to exist there must be models \({\mathcal {I}}_1\) of \(T_1\) and \({\mathcal {I}}_2\) of \(T_2\) that agree on the interpretation they give to the sort and function symbols shared by \(\varSigma _1\) and \(\varSigma _2\).

  3. In the sense that all occurrences of f in P are applied to some arguments.

  4. Note that since \(P[f, \varvec{x}]\) is first-order, all occurrences of \(\lambda \varvec{x}\, t\) in \(P[\lambda \varvec{x}\, t, \varvec{x}]\) can be \(\beta \)-reduced.

  5. These are versions that either do not have function symbols denoting partial functions or make those functions total in some way.

  6. An example of a property that is not single-invocation is \(\forall x_1\,x_2\, f( x_1, x_2 ) \approx f( x_2, x_1 )\), stating that f is a commutative function.

  7. Note that \(Q[\varvec{x}, f(\varvec{x})]\) is a formula over the variables f and \(\varvec{x}\) and so it has the form \(P[f, \varvec{x}]\) as in the definition of \({\mathbf {P}}\).

  8. That is, \(\lnot ^{\mathsf {Bool}\, \mathsf {Bool}}\) interpreted as Boolean negation, \(\wedge ^{\mathsf {Bool}\, \mathsf {Bool}\, \mathsf {Bool}}\) as Boolean conjunction, \(\approx ^{\sigma \, \sigma \, \mathsf {Bool}}\) as the equality function, and so on.

  9. cvc4 ’s solver for the theory of datatypes can do both things.

  10. We make this assumption to simplify the presentation. The SyGuS language [37] defines a more general class of restrictions R for which this is not necessarily possible.

  11. The selector \(\mathsf {s}_{c,i}\) is such that \(\models _{D} \mathsf {s}_{c,i}(c(d_1,\ldots ,d_n)) \approx d_i\) for all constructor terms \(d_1,\ldots ,d_n\) of respective type \(\delta _1,\ldots ,\delta _n\). The tester \(\mathsf {is}_{c}\) is such that, for all terms d of type \(\delta \), \(\models _{D} \mathsf {is}_{c}(d) \approx \mathsf {tt}\) iff the top symbol of d is c.

  12. Note that this assumption is pragmatic and can be made arbitrarily mild. For instance, depending on the theory, in the worst case one can always consider every term to be irreducible.

  13. CVC4 is available at http://cvc4.cs.stanford.edu.

  14. A detailed summary of our results can be found at http://lara.epfl.ch/w/cvc4-synthesis.

  15. As an exception, for the array class of benchmarks, cvc4+si found solutions that were rewritten into exponentially larger ones during solution reconstruction to meet the syntactic restrictions.

  16. These benchmarks, as contributed to the SyGuS benchmark set, use integer variables only; they were generated by expanding fixed-size arrays and actually contain no array operations.

  17. cvc4 has a portfolio mode that allows it to run multiple configurations at the same time.

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 R, Martin MMK, Raghothaman M, Stergiou C, Tripakis S, Udupa A (2014) Synthesizing finite-state protocols from scenarios and requirements. In: Yahav E (ed) Haifa verification conference, LNCS, vol 8855, pp 75–91. Springer. doi:10.1007/978-3-319-13338-6_7

    Chapter  Google Scholar 

  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 (2013) 6 years of SMT-COMP. JAR 50(3):243–277. doi:10.1007/s10817-012-9246-5

    Article  Google Scholar 

  7. Barrett C, Shikanian I, Tinelli C (2007) An abstract decision procedure for satisfiability in the theory of inductive data types. J Satisf Boolean Model Comput 3:21–46

    MathSciNet  MATH  Google Scholar 

  8. Bjørner N (2010) Linear quantifier elimination as an abstract decision procedure. In: Giesl J, Hähnle R (eds) IJCAR, LNCS, vol 6173, pp 316–330. Springer. doi:10.1007/978-3-642-14203-1_27

    Chapter  Google Scholar 

  9. Bloem R, Jobstmann B, Piterman N, Pnueli A, Sa’ar Y (2012) Synthesis of reactive(1) designs. J Comput Syst Sci 78(3):911–938. doi:10.1016/j.jcss.2011.08.007

    Article  MathSciNet  MATH  Google Scholar 

  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 (1986) Implementing mathematics with the Nuprl proof development system. Prentice Hall, Englewood Cliffs

    Google Scholar 

  11. Cousot P (2005) Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot R (ed) VMCAI, LNCS, vol 3385. Springer, pp 1–24. doi:10.1007/978-3-540-30579-8_1

    Google Scholar 

  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

  13. Detlefs D, Nelson G, Saxe, JB (2003) Simplify: a theorem prover for program checking. Technical report. J ACM

  14. Dutertre B (2015) Solving exists/forall problems with yices. In: Workshop on satisfiability modulo theories

  15. Finkbeiner B, Schewe S (2013) Bounded synthesis. STTT 15(5–6):519–539. doi:10.1007/s10009-012-0228-z

    Article  MATH  Google Scholar 

  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

  17. Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Proceedings of CAV’09, LNCS, vol 5643. Springer, pp 306–320. doi:10.1007/978-3-642-02658-4_25

    Chapter  Google Scholar 

  18. Green CC (1969) Application of theorem proving to problem solving. In: Walker DE, Norton LM (eds) IJCAI. William Kaufmann, Los Altos, pp 219–240

    Google Scholar 

  19. Jacobs S, Kuncak V (2011) Towards complete reasoning about axiomatic specifications. Verification, model checking, and abstract interpretation. Springer, Berlin, pp 278–293

    Chapter  Google Scholar 

  20. Janota M, Klieber W, Marques-Silva J, Clarke E (2012) Solving QBF with counterexample guided refinement. In: International conference on theory and applications of satisfiability testing. Springer Berlin, pp 114–128 (2012)

    Chapter  Google Scholar 

  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

  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 E, Koukoutos M, Kuncak V (2015) Deductive program repair. In: Kroening D, Pasareanu CS (eds) CAV, LNCS, vol 9207. Springer, pp 217–233. doi:10.1007/978-3-319-21668-3_13

    Chapter  Google Scholar 

  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

  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 (2012) Software synthesis procedures. CACM 55(2):103–111. doi:10.1145/2076450.2076472

    Article  Google Scholar 

  28. Kuncak V, Mayer M, Piskac R, Suter P (2013) Functional synthesis for linear arithmetic and sets. STTT 15(5–6):455–474. doi:10.1007/s10009-011-0217-7

    Article  Google Scholar 

  29. Madhavan R, Kuncak V (2014) Symbolic resource bound inference for functional programs. In: Biere A, Bloem R (eds) CAV, LNCS, vol 8559. Springer, pp 762–778. doi:10.1007/978-3-319-08867-9_51

    Chapter  Google Scholar 

  30. Manna Z, Waldinger RJ (1980) A deductive approach to program synthesis. TOPLAS 2(1):90–121. doi:10.1145/357084.357090

    Article  MATH  Google Scholar 

  31. Monniaux D (2010) Quantifier elimination by lazy model enumeration. In: Touili T, Cook B, Jackson P (eds) CAV, LNCS, vol 6174. Springer, pp 585–599. doi:10.1007/978-3-642-14295-6_51

    Chapter  Google Scholar 

  32. de Moura LM, Bjørner N (2007) Efficient e-matching for SMT solvers. In: F. Pfenning (ed) CADE, LNCS, vol 4603. Springer, pp 183–198. doi:10.1007/978-3-540-73595-3_13

    Chapter  Google Scholar 

  33. Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J ACM 53(6):937–977

    Article  MathSciNet  Google Scholar 

  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

  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

  39. Reynolds A, King T, Kuncak V (2015) An instantiation-based approach for solving quantified linear arithmetic. CoRR arXiv:1510.02642

  40. Reynolds A, Tinelli C, Goel A, Krstić S, Deters M, Barrett C (2013) Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina MP (ed) Proceedings of the 24th international conference on automated deduction, Lake Placid, NY, USA, Lecture notes in computer science, vol 7898. Springer, pp 377–391

    Chapter  Google Scholar 

  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 S, Garg P, Madhusudan P (2015) Alchemist: learning guarded affine functions. In: Kroening D, Psreanu CS (eds) Computer aided verification, Lecture notes in computer science, vol 9206, pp 440–446. Springer. doi:10.1007/978-3-319-21690-4_26

    Chapter  Google Scholar 

  44. Schkufza E, Sharma R, Aiken A (2013) Stochastic superoptimization. SIGPLAN Not 48(4):305–316. doi:10.1145/2499368.2451150

    Article  Google Scholar 

  45. Solar-Lezama A (2013) Program sketching. STTT 15(5–6):475–495. doi:10.1007/s10009-012-0249-7

    Article  Google Scholar 

  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 (2013) Template-based program verification and program synthesis. STTT 15(5–6):497–518. doi:10.1007/s10009-012-0223-4

    Article  Google Scholar 

  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 J, Axelsson E (2012) Combining deep and shallow embedding for EDSL. In: Trends in functional programming—13th international symposium, TFP 2012, Revised selected papers, pp 21–36, St. Andrews, UK, 12–14 June 2012. doi:10.1007/978-3-642-40447-4_2

    Google Scholar 

  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

  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 M, Nipkow T (2004) Certifying machine code safety: shallow versus deep embedding. In: Theorem proving in higher order logics, 17th international conference, TPHOLs 2004, Proceedings, pp 305–320, Park City, UT, USA, 14–17 Sept 2004. doi:10.1007/978-3-540-30142-4_22

    Google Scholar 

  53. Wintersteiger CM, Hamadi Y, De Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42(1):3–23

    Article  Google Scholar 

Download references

Acknowledgements

We would like to thank Liana Hadarean for helpful discussions on the normal form used in cvc4 for bit vector terms, and Tim King for his contributions to the ground linear arithmetic solver in CVC4. Funding was provided by European Research Council (BE) (Grant No. 306484), Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung (CH) (Grant No. 200020_159949), Directorate for Computer and Information Science and Engineering (Grant No. CNS 1228768).

Author information

Authors and Affiliations

  1. École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland

    Andrew Reynolds & Viktor Kuncak

  2. Department of Computer Science, The University of Iowa, Iowa City, IA, USA

    Andrew Reynolds & Cesare Tinelli

  3. Department of Computer Science, Stanford University, Stanford, CA, USA

    Clark Barrett

  4. Department of Computer Science, New York University, New York, NY, USA

    Morgan Deters

Authors
  1. Andrew Reynolds
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viktor Kuncak
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Cesare Tinelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Clark Barrett
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Morgan Deters
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cesare Tinelli.

Additional information

In memory of Morgan Deters who passed away unexpectedly in 2015.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Reynolds, A., Kuncak, V., Tinelli, C. et al. Refutation-based synthesis in SMT. Form Methods Syst Des 55, 73–102 (2019). https://doi.org/10.1007/s10703-017-0270-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-017-0270-2

Keywords

Search

Navigation