Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 2/2019

16.02.2017

Refutation-based synthesis in SMT

verfasst von: Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, Morgan Deters

Erschienen in: Formal Methods in System Design | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Nächster Artikel Synthesizing adaptive test strategies from temporal logic specifications

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
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.
 
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.
 
Literatur
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.
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 CrossRef
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.
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–46MathSciNetMATH
8.
9.
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
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
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.
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.
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
19.
Jacobs S, Kuncak V (2011) Towards complete reasoning about axiomatic specifications. Verification, model checking, and abstract interpretation. Springer, Berlin, pp 278–293CrossRef
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)CrossRef
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.
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.
27.
28.
29.
30.
31.
32.
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–977MathSciNetCrossRef
34.
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.
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–391CrossRef
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 CrossRef
44.
45.
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.
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
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
53.
Wintersteiger CM, Hamadi Y, De Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42(1):3–23CrossRef
Metadaten
Titel
Refutation-based synthesis in SMT
verfasst von
Andrew Reynolds
Viktor Kuncak
Cesare Tinelli
Clark Barrett
Morgan Deters
Publikationsdatum
16.02.2017
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 2/2019
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0270-2