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 3/2017

03.08.2017

Solving quantified linear arithmetic by counterexample-guided instantiation

verfasst von: Andrew Reynolds, Tim King, Viktor Kuncak

Erschienen in: Formal Methods in System Design | Ausgabe 3/2017

Einloggen

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

search-config
loading …

Abstract

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic and linear integer arithmetic formulas with one quantifier alternation. We discuss extensions of these techniques for handling mixed real and integer arithmetic, and to formulas with arbitrary quantifier alternations. For the latter, we use a novel strategy that handles quantified formulas that are not in prenex normal form, which has advantages with respect to existing approaches. All of these techniques can be integrated within the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation in the SMT solver cvc4 outperforms existing tools for quantified linear arithmetic.
Vorheriger Artikel raSAT: an SMT solver for polynomial constraints
Nächster Artikel NP-completeness of small conflict set generation for congruence closure

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
In the parlance of [16], \(\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}\) selects a feasible j value using the calculation of \(\rho \) and avoids introducing the \(F_{\pm \infty }\) cases by introducing the no bounds case (\(n = 0, m=0\)) and always favoring bounds when one exists.
 
2
For example, notice that \(\lnot \forall x_1\, \exists x_2\, \forall x_3\, \exists x4\, \varphi \) is equivalent to \(\lnot \forall x_1\, \lnot \forall x_2\, \lnot \forall x_3\, \lnot \forall x_4\, \lnot \varphi \).
 
4
The solver cvc4-sc16 won the \(\mathrm {LRA} \) and \(\mathrm {LIA} \) divisions of SMT COMP 2016. The TFA division of CASC J8 includes problems that combine arithmetic and uninterpreted functions, where the techniques in this paper are only partially applicable. Vampire won this division, and cvc4 came in \(3\mathrm{rd}\).
 
5
For 2 templates, both z3 and cvc4 took more than 5 s to solve for both cases of \(F \in \{ \top , \bot \}\), and for 1 template, z3 timed out when F was \(\bot \).
 
Literatur
1.
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. To Appear in Marktoberdorf NATO proceedings
2.
3.
4.
5.
Bansal K, Reynolds A, King T, Barrett C, Wies T (2015) Deciding local theory extensions via e-matching. In: Computer aided verification (CAV), Springer
6.
Barrett C, Conway C, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) Cvx4. In: Computer aided verification (CAV), Springer
7.
8.
Baumgartner P (2015) Smttotptp a converter for theorem proving formats. In: CADE-25, Lecture notes in computer science, vol 9195. Springer
9.
10.
Beyene TA, Chaudhuri S, Popeea C, Rybalchenko A (2014) A constraint-based approach to solving games on infinite graphs. In: POPL, pp 221–234
11.
Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified Horn clauses. In: CAV, pp 869–882
12.
Bjørner N (2010) Linear quantifier elimination as an abstract decision procedure. In Giesl J, Hähnle R (eds) IJCAR, LNCS, vol 6173. Springer, pp 316–330
13.
Bjørner N, Janota M (2015) Playing with quantified satisfaction. In: 20th international conferences on logic for programming, artificial intelligence and reasoning—short presentations, LPAR 2015, Suva, Fiji, 24–28 November 2015, pp 15–27
14.
Bjørner N, McMillan KL, Rybalchenko A (2012) Program verification as satisfiability modulo theories. In: SMT@IJCAR, pp 3–11
15.
16.
Cooper DC (1972) Theorem proving in arithmetic without multiplication. In: Meltzer B, Michie D (eds) Machine intelligence, vol 7. Edinburgh University Press, Edinburgh, pp 91–100
17.
de Moura LM, Bjørner N (2007) Efficient e-matching for SMT solvers. In: Pfenning F, (ed) CADE, LNCS, vol 4603. Springer, pp 183–198
18.
Detlefs D, Nelson G, Saxe JB (2003) Simplify: a theorem prover for program checking. J. ACM, Technical report
19.
Dutertre B (2015) Solving exists/forall problems with yices. In: Workshop on Satisfiability modulo theories
20.
Farzan A Kincaid Z (2016) Linear arithmetic satisfiability via strategy improvement. In: Proceedings of the twenty-fifth international joint conference on artificial intelligence, IJCAI 2016, New York, NY, USA, 9–15 July 2016, pp 735–743
21.
Fedyukovich G, Gurfinkel A, Sharygina N (2015) Automated discovery of simulation between programs. In: Logic for programming, artificial intelligence, and reasoning—20th international conference, LPAR-20 2015, Suva, Fiji, 24–28 November 2015, Proceedings, pp 606–621
22.
Feferman S, Vaught RL (1959) The first order properties of products of algebraic systems. Fundam Math 47:57–103CrossRefMATH
23.
Ferrante J, Rackoff CW (1979) The computational complexity of logical theories, lecture notes in mathematics, vol 718. Springer, BerlinCrossRefMATH
24.
Ganzinger H, Korovin K (2003) New directions in instantiation-based theorem proving. In: Logic in computer science, 2003. IEEE
25.
Ge Y, Barrett C, Tinelli C (2007) Solving quantified verification conditions using satisfiability modulo theories. In CADE, LNCS, vol 4603. Springer
26.
Ge Y, de Moura L (2009) Complete instantiation for quantified formulas in satisfiability modulo theories. In: Proceedings of CAV’09, LNCS, vol 5643. Springer
27.
Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI, pp 405–416
28.
Heizmann M, Dietsch D, Leike J, Musa B, Podelski A (2015) Ultimate automizer with array interpolation. In: TACAS
29.
Hodges W (1993) Model Theory, encyclopedia of mathematics and its applications, vol 42. Cambridge University Press, Cambridge
30.
Jacobs S (2009) Incremental instance generation in local reasoning. In: CAV ’09, Springer, Berlin, Heidelberg, pp 368–382
31.
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, Heidelberg, pp 114–128
32.
Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification, Springer
33.
Kozen D (2006) Theory of computation. Springer, BerlinMATH
34.
Kuncak V, Mayer M, Piskac R, Suter P (2010) Complete functional synthesis. In: Zorn BG, Aiken A (eds) PLDI. ACM, New york, pp 316–329
35.
Kuncak V, Rinard M (2003) Structural subtyping of non-recursive types is decidable. In: Eighteenth annual IEEE symposium on logic in computer science (LICS). IEEE
36.
37.
Lopes NP, Monteiro J (2014) Weakest precondition synthesis for compiler optimizations. In: VMCAI 2014, pp 203–221
38.
Maher MJ (1988) Complete axiomatizations of the algebras of the finite, rational, and infinite trees. In: IEEE symposium on logic in computer science
39.
Mal’cev AI (1971) The metamathematics of algebraic systems, studies in logic and the foundations of mathematics, vol 66. North-Holland, Amsterdam
40.
Monniaux D (2009) Automatic modular abstractions for linear constraints. In: POPL 2009, pp 140–151
41.
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
42.
43.
Nipkow T (2008) Linear quantifier elimination. In: Automated reasoning, pp 18–33
44.
Phan A, Bjørner N, Monniaux D (2012) Anatomy of alternating quantifier satisfiability (work in progress). In SMT 2012
45.
Platzer A, Quesel J-D, Rümmer P (2009) Real world verification. In: Automated Deduction–CADE-22, Springer, Berlin, Heidelberg, pp 485–501
46.
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
47.
Pugh W (1991) The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: ACM/IEEE conference supercomputing
48.
Reddy CR, Loveland DW (1978) Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, ACM Press, pp 320–325
49.
Reger G, Suda M, Voronkov A (2015) Playing with avatar. In: Automated deduction-CADE-25, Springer, pp 399–415
50.
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, San Francisco, CA, USA, 18-24 July 2015, Proceedings, Part II, pp 198–216
51.
Reynolds A, Tinelli C, Moura LD (2014) Finding conflicting instances of quantified formulas in SMT. In: Formal methods in computer-aided design (FMCAD)
52.
53.
Saha S, Garg P, Madhusudan P (2015) Alchemist: learning guarded affine functions. In: Computer aided verification—27th international conference, CAV 2015, San Francisco, CA, USA, 18–24 July 2015, Proceedings, Part I, pp 440–446
54.
Scholl C, Disch S, Pigorsch F, Kupferschmid S (2008) Using an smt solver and craig interpolation to detect and remove redundant linear constraints in representations of non-convex polyhedra. In: SMT, ACM, pp 18–26
55.
Skolem T (1919) Untersuchungen über die Axiome des Klassenkalküls and über “Produktations- und Summationsprobleme”, welche gewisse Klassen von Aussagen betreffen. Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, no. 3, Oslo
56.
Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: ISSAC 2011, pp 329–336
57.
Sturm T, Weispfenning V (2002) Quantifier elimination in term algebras: the case of finite languages. TUM Muenchen, In: Computer algebra in scientific computing (CASC)
58.
Sutcliffe G (2009) The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J Autom Reason 43(4):337–362MathSciNetCrossRefMATH
59.
Sutcliffe G (2016) The CADE ATP system competition—CASC. AI Magazine 37(2):99–101CrossRefMATH
60.
Tarski A (1949) Arithmetical classes and types of algebraically closed and real-closed fields. Bull Am Math Soc 55(1):64
61.
Tarski A (1949) Arithmetical classes and types of boolean algebras. Bull Am Math Soc 55(64):1192
62.
Treinen R (1997) Feature trees over arbitrary structures, chapter 7. In: Blackburn P, de Rijke M (eds) Specifying syntactic structures. CSLI Publications and FoLLI, Stanford
63.
64.
Weispfenning V (1997) Complexity and uniformity of elimination in Presburger arithmetic. In: ISSAC ’97, New York, NY, USA, ACM, pp 48–53
65.
Weispfenning V (1999) Mixed real-integer linear quantifier elimination. In: Proceedings of the 1999 international symposium on symbolic and algebraic computation, ISSAC ’99, New York, NY, USA, ACM, pp 129–136
66.
Wintersteiger CM, Hamadi Y, De Moura L (2013) Efficiently solving quantified bit-vector formulas. Form Methods Syst Des 42(1):3–23CrossRefMATH
Metadaten
Titel
Solving quantified linear arithmetic by counterexample-guided instantiation
verfasst von
Andrew Reynolds
Tim King
Viktor Kuncak
Publikationsdatum
03.08.2017
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2017
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0290-y

Weitere Artikel der Ausgabe 3/2017

Formal Methods in System Design 3/2017 Zur Ausgabe

OriginalPaper

Cardinality constraints for arrays (decidability results and applications)

OriginalPaper

NP-completeness of small conflict set generation for congruence closure

OriginalPaper

New techniques for linear arithmetic: cubes and equalities

OriginalPaper

raSAT: an SMT solver for polynomial constraints

OriginalPaper

Compositional entailment checking for a fragment of separation logic

OriginalPaper

Propagation based local search for bit-precise reasoning