Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 3/2017

03-08-2017

Solving quantified linear arithmetic by counterexample-guided instantiation

Authors: Andrew Reynolds, Tim King, Viktor Kuncak

Published in: Formal Methods in System Design | Issue 3/2017

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article raSAT: an SMT solver for polynomial constraints
next article NP-completeness of small conflict set generation for congruence closure

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
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 \).
 
Literature
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.
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.
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
Metadata
Title
Solving quantified linear arithmetic by counterexample-guided instantiation
Authors
Andrew Reynolds
Tim King
Viktor Kuncak
Publication date
03-08-2017
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2017
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0290-y

Other articles of this Issue 3/2017

Formal Methods in System Design 3/2017 Go to the issue

OriginalPaper

NP-completeness of small conflict set generation for congruence closure

OriginalPaper

Propagation based local search for bit-precise reasoning

OriginalPaper

Compositional entailment checking for a fragment of separation logic

OriginalPaper

New techniques for linear arithmetic: cubes and equalities

OriginalPaper

raSAT: an SMT solver for polynomial constraints

OriginalPaper

Cardinality constraints for arrays (decidability results and applications)

Premium Partner

    Image Credits