article

Solving quantified linear arithmetic by counterexample-guided instantiation

Authors:

Andrew Reynolds,

Viktor KuncakAuthors Info & Claims

Formal Methods in System Design, Volume 51, Issue 3

Pages 500 - 532

https://doi.org/10.1007/s10703-017-0290-y

Published: 01 December 2017 Publication History

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.

References

[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]

Alur R, Fisman D, Singh R, Solar-Lezama A (2016) Results and analysis of sygus-comp'15. arXiv preprint arXiv:1602.01170

[3]

Alur R, Radhakrishna A, Udupa A (2016) Scaling enumerative program synthesis via divide and conquer. Technical report, UPenn https://www.seas.upenn.edu/~arjunrad/publications/eusolver_report.pdf

[4]

Backofen R (1995) A complete axiomatization of a theory with feature and arity constraints. J Log Program 24:37---72

[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]

Barrett C, Stump A, Tinelli C (2010) The satisfiability modulo theories library (SMT-LIB). http://www.SMT-LIB.org

[8]

Baumgartner P (2015) Smttotptp a converter for theorem proving formats. In: CADE-25, Lecture notes in computer science, vol 9195. Springer

[9]

Berman L (1980) The complexity of logical theories. Theor Comput Sci 11(1):71---77

Digital Library

[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

Digital Library

[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

Digital Library

[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]

Comon H, Delor C (1994) Equational formulae with membership constraints. Inf Comput 112(2):167---216

Digital Library

[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

Digital Library

[18]

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

Digital Library

[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

Digital Library

[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

Digital Library

[22]

Feferman S, Vaught RL (1959) The first order properties of products of algebraic systems. Fundam Math 47:57---103

[23]

Ferrante J, Rackoff CW (1979) The computational complexity of logical theories, lecture notes in mathematics, vol 718. Springer, Berlin

[24]

Ganzinger H, Korovin K (2003) New directions in instantiation-based theorem proving. In: Logic in computer science, 2003. IEEE

Digital Library

[25]

Ge Y, Barrett C, Tinelli C (2007) Solving quantified verification conditions using satisfiability modulo theories. In CADE, LNCS, vol 4603. Springer

Digital Library

[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

Digital Library

[27]

Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI, pp 405---416

Digital Library

[28]

Heizmann M, Dietsch D, Leike J, Musa B, Podelski A (2015) Ultimate automizer with array interpolation. In: TACAS

Digital Library

[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

Digital Library

[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

Digital Library

[32]

Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification, Springer

Digital Library

[33]

Kozen D (2006) Theory of computation. Springer, Berlin

Digital Library

[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

Digital Library

[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

Digital Library

[36]

Loos R, Weispfenning V (1993) Applying linear quantifier elimination. Comput J 36(5):450---462

[37]

Lopes NP, Monteiro J (2014) Weakest precondition synthesis for compiler optimizations. In: VMCAI 2014, pp 203---221

Digital Library

[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

Digital Library

[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

Digital Library

[42]

Mostowski A (1952) On direct products of theories. J Symb Logic 17(1):1---31

[43]

Nipkow T (2008) Linear quantifier elimination. In: Automated reasoning, pp 18---33

Digital Library

[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

Digital Library

[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

Digital Library

[48]

Reddy CR, Loveland DW (1978) Presburger arithmetic with bounded quantifier alternation. In: ACM STOC, ACM Press, pp 320---325

Digital Library

[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)

Digital Library

[52]

Rybina T, Voronkov A (2001) A decision procedure for term algebras with queues. ACM Trans Comput Logic (TOCL) 2(2):155---181

Digital Library

[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

Digital Library

[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

Digital Library

[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---362

Digital Library

[59]

Sutcliffe G (2016) The CADE ATP system competition--CASC. AI Magazine 37(2):99---101

[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

Digital Library

[63]

Walukiewicz I (2002) Monadic second-order logic on tree-like structures. Theor Comput Sci 275(1---2):311---346

Digital Library

[64]

Weispfenning V (1997) Complexity and uniformity of elimination in Presburger arithmetic. In: ISSAC '97, New York, NY, USA, ACM, pp 48---53

Digital Library

[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

Digital Library

[66]

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

Digital Library

Cited By

Barrett CTinelli CBarbosa HNiemetz APreiner MReynolds AZohar Y(2024)Satisfiability Modulo Theories: A Beginner’s TutorialFormal Methods10.1007/978-3-031-71177-0_31(571-596)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_31
Jakubův JJanota MUrban J(2024)Solving Hard Mizar Problems with Instantiation and Strategy InventionIntelligent Computer Mathematics10.1007/978-3-031-66997-2_18(315-333)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_18
Murphy CKincaid Z(2024)Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy ImprovementComputer Aided Verification10.1007/978-3-031-65627-9_5(89-109)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_5
Show More Cited By

Recommendations

Approximating Quantified SMT-Solving with SAT
SSIRI-C '11: Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - Companion

Satisfiability Modulo Theories (SMT) is an extension of SAT towards FOL. SMT solvers have proven highly scalable and efficient for problems based on some ground theorems. However, SMT problems involving quantifiers and combination of theorems is a long-...
Solving quantified verification conditions using satisfiability modulo theories

First-order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first-order automated theorem proving (ATP) and automated theorem proving based on ...
Bounds on the automata size for Presburger arithmetic

Automata provide a decision procedure for Presburger arithmetic. However, until now only crude lower and upper bounds were known on the sizes of the automata produced by the automata-based approach for Presburger arithmetic. In this article, we give an ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 51, Issue 3

December 2017

206 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2017 Springer Science+Business Media, LLC, part of Springer Nature.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 December 2017

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Barrett CTinelli CBarbosa HNiemetz APreiner MReynolds AZohar Y(2024)Satisfiability Modulo Theories: A Beginner’s TutorialFormal Methods10.1007/978-3-031-71177-0_31(571-596)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_31
Jakubův JJanota MUrban J(2024)Solving Hard Mizar Problems with Instantiation and Strategy InventionIntelligent Computer Mathematics10.1007/978-3-031-66997-2_18(315-333)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_18
Murphy CKincaid Z(2024)Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy ImprovementComputer Aided Verification10.1007/978-3-031-65627-9_5(89-109)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_5
Habermehl PHavlena VHečko MHolík LLengál O(2024)Algebraic Reasoning Meets Automata in Solving Linear Integer ArithmeticComputer Aided Verification10.1007/978-3-031-65627-9_3(42-67)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_3
Abate ABarbosa HBarrett CDavid CKesseli PKroening DPolgreen EReynolds ATinelli C(2023)Synthesising Programs with Non-trivial ConstantsJournal of Automated Reasoning10.1007/s10817-023-09664-467:2Online publication date: 13-May-2023
https://dl.acm.org/doi/10.1007/s10817-023-09664-4
Stoilkovska IKonnov IWidder JZuleger F(2022)Verifying safety of synchronous fault-tolerant algorithms by bounded model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-021-00637-924:1(33-48)Online publication date: 1-Feb-2022
https://dl.acm.org/doi/10.1007/s10009-021-00637-9
Voigt M(2021)Decidable First-Order Fragments of Linear Rational Arithmetic with Uninterpreted PredicatesJournal of Automated Reasoning10.1007/s10817-020-09567-865:3(357-423)Online publication date: 1-Mar-2021
https://dl.acm.org/doi/10.1007/s10817-020-09567-8
Backeman PRümmer PZeljić A(2021)Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmeticFormal Methods in System Design10.1007/s10703-021-00372-657:2(121-156)Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s10703-021-00372-6
Niemetz APreiner MReynolds ABarrett CTinelli C(2021)On solving quantified bit-vector constraints using invertibility conditionsFormal Methods in System Design10.1007/s10703-020-00359-957:1(87-115)Online publication date: 1-Jul-2021
https://dl.acm.org/doi/10.1007/s10703-020-00359-9
Wu HFarrell M(2021)A formal approach to finding inconsistencies in a metamodelSoftware and Systems Modeling (SoSyM)10.1007/s10270-020-00849-820:4(1271-1298)Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s10270-020-00849-8
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents