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/2016

07-12-2016

A layered algorithm for quantifier elimination from linear modular constraints

Authors: Ajith K. John, Supratik Chakraborty

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

Log in

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

search-config
loading …

Abstract

Linear equalities, disequalities and inequalities on fixed-width bit-vectors, collectively called linear modular constraints, form an important fragment of the theory of fixed-width bit-vectors. We present a practically efficient and bit-precise algorithm for quantifier elimination from conjunctions of linear modular constraints. Our algorithm uses a layered approach, whereby sound but incomplete and cheaper layers are invoked first, and expensive but complete layers are called only when required. We then extend this algorithm to work with arbitrary Boolean combinations of linear modular constraints as well. Experiments on an extensive set of benchmarks demonstrate that our techniques significantly outperform alternative quantifier elimination techniques based on bit-blasting and linear integer arithmetic.
previous article From LTL to deterministic automata

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
Literature
1.
Ax J, Kochen S (1965) Diophantine problems over local fields II. A complete set of axioms for p-adic number theory. Am J Math 87(3):631–648MathSciNetCrossRefMATH
2.
Babic D, Musuvathi M (2005) Modular arithmetic decision procedure. Technical report TR-2005-114, Microsoft Research
3.
Bierre A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Proceedings of international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp 193–207
4.
Bjørner N (2010) Linear quantifier elimination as an abstract decision procedure. In: Proceedings of international joint conference on automated reasoning (IJCAR), pp 316–330
5.
Bjørner N, Pichora M (1998) Deciding fixed and non-fixed size bit-vectors. In: Proceedings of international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp 376–392
6.
Bjørner N, Janota M (2015) Playing with quantified satisfaction. In: Proceedings of international conferences on logic for programming, artificial intelligence and reasoning (LPAR)—short presentations, pp 15–27
7.
Bjørner N, Blass A, Gurevich Y, Musuvathi M (2008) Modular difference logic is hard. CoRR abs/0811.0987
8.
Brinkmann R, Drechsler R (2002) RTL-datapath verification using integer linear programming. In: Proceedings of IEEE VLSI design conference, pp 741–746
9.
Bruttomesso R, Sharygina N (2009) A scalable decision procedure for fixed-width bit-vectors. In: Proceedings of international conference on computer-aided design (ICCAD), pp 13–20
10.
Bryant R (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677–691CrossRefMATH
11.
Cavada R, Cimatti A, Franzen A, Kalyanasundaram K, Roveri M, Shyamasundar RK (2007) Computing predicate abstractions by integrating BDDs and SMT solvers. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 69–76
12.
Chaki S, Gurfinkel A, Strichman O (2009) Decision diagrams for linear arithmetic. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 53–60
13.
Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
14.
Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of international conference on computer aided verification (CAV), pp 154–169
15.
Cohen P (1969) Decision procedures for real and p-adic fields. Commun Pure Appl Logic 25:213–231
16.
Cooper D (1972) Theorem proving in arithmetic without multiplication. Mach Intell 7:91–99MATH
17.
18.
Cyrluk D, Möller M, Rueß H (1997) An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Proceedings of international conference on computer aided verification (CAV), pp 60–71
19.
Damm W, Dierks H, Disch S, Hagemann W, Pigorsch F, Scholl C, Waldmann U, Wirtz B (2012) Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Sci Comput Program 77(10–11):1122–1150CrossRefMATH
20.
21.
Das S (2003) Predicate abstraction. PhD thesis, Stanford University
22.
23.
de Moura L, Bjørner N (2007) Relevancy propagation. Technical report TR-2007-140, Microsoft Research
24.
de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp 337–340
25.
Déharbe D, Fontaine P, Berre DL, Mazure B (2013) Computing prime implicants. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 46–52
26.
Ferrante J, Rackoff C (1975) A decision procedure for the first order theory of real addition with order. Soc Ind Appl Math (SIAM) J Comput 4(1):69–76MathSciNetMATH
27.
Ganesh V, Dill D (2007) A decision procedure for bit-vectors and arrays. In: Proceedings of international conference on computer aided verification (CAV), pp 519–531
28.
Ganesh V, Berezin S, Dill D (2002) Deciding Presburger arithmetic by model checking and comparisons with other methods. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 171–186
29.
Gange G, Søndergaard H, Stuckey P, Schachte P (2013) Solving difference constraints over modular arithmetic. In: Proceedings of international conference on automated deduction (CADE), pp 215–230
30.
Gotlieb A, Leconte M, Marre B (2010) Constraint solving on modular integers. In: Proceedings of ninth international workshop on constraint modelling and reformulation (ModRef) co-located with international conference on principles and practice of constraint programming (CP)
31.
Griggio A (2011) Effective word-level interpolation for software verification. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 28–36
32.
Hadarean L, Bansal K, Jovanovic D, Barret C, Tinelli C (2014) A tale of two solvers: eager and lazy approaches to bit-vectors. In: Proceedings of international conference on computer aided verification (CAV), pp 680–695
33.
Howell JA, Gregory RT (1969) An algorithm for solving linear algebraic equations using residue arithmetic I. BIT Numer Math 9(3):200–224MathSciNetCrossRefMATH
34.
Huang C, Cheng K (2000) Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques. In: Proceedings of ACM/IEEE design automation conference (DAC), pp 118–123
35.
Jain H, Clarke EM, Grumberg O (2008) Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. In: Proceedings of international conference on computer aided verification (CAV), pp 254–267
36.
John A, Chakraborty S (2011) A quantifier elimination algorithm for linear modular equations and disequations. In: Proceedings of international conference on computer aided verification (CAV), pp 486–503
37.
John A, Chakraborty S (2013) Extending quantifier elimination to linear inequalities on bit-vectors. In: Proceedings of international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp 78–92
38.
Kapur D (2006) A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. J Syst Sci Complex 19(3):307–330MathSciNetCrossRefMATH
39.
Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Proceedings of international conference on computer aided verification (CAV), pp 17–34
40.
Kroening D, Strichman O (2008) Decision procedures: an algorithmic point of view. Springer, BerlinMATH
41.
Lahiri S, Nieuwenhuis R, Oliveras A (2006) SMT techniques for fast predicate abstraction. In: Proceedings of international conference on computer aided verification (CAV), pp 424–437
42.
43.
Mishchenko A, Chatterjee S, Jiang R, Brayton R (2005) FRAIGs: a unifying representation for logic synthesis and verification. Technical report, EECS Department, UC Berkeley
44.
Monniaux D (2008) A quantifier elimination algorithm for linear real arithmetic. In: Proceedings of international conference on logic for programming artificial intelligence and reasoning (LPAR), pp 243–257
45.
Monniaux D (2010) Quantifier elimination by lazy model enumeration. In: Proceedings of international conference on computer aided verification (CAV), pp 585–599
46.
Müller-Olm M, Seidl H (2007) Analysis of modular arithmetic. ACM Trans Program Lang Syst (TOPLAS) 29(5):29
47.
Niemetz A, Preiner M, Biere A (2014) Turbo-charging lemmas on demand with don’t care reasoning. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 179–186
48.
Nipkow T (2008) Linear quantifier elimination. In: Proceedings of international joint conference on automated reasoning (IJCAR), pp 18–33
49.
Owre S, Rushby J, Shankar N (1992) PVS: A prototype verification system. In: Proceedings of international conference on automated deduction (CADE), pp 748–752
50.
Phan A, Bjørner N, Monniaux D (2012) Anatomy of alternating quantifier satisfiability (work in progress). In: Proceedings of SMT workshop at international joint conference on automated reasoning (SMT@IJCAR), pp 120–130
51.
Pugh W (1992) The Omega test: a fast and practical integer programming algorithm for dependence analysis. Commun ACM 35(8):102–114CrossRef
52.
53.
54.
Szabo N, Tanaka R (1967) Residue arithmetic and its applications to computer technology. McGraw-Hill, New YorkMATH
55.
Tew N, Kalla P, Shekhar N, Gopalakrishnan S (2008) Verification of arithmetic datapaths using polynomial function models and congruence solving. In: Proceedings of international conference on computer-aided design (ICCAD), pp 122–128
56.
Veanes M, Bjørner N, Nachmanson L, Bereg S (2014) Monadic decomposition. In: Proceedings of international conference on computer aided verification (CAV), pp 628–645
57.
Wintersteiger C, Hamadi Y, de Moura L (2010) Efficiently solving quantified bit-vector formulas. In: Proceedings of international conference on formal methods in computer-aided design (FMCAD), pp 239–246
Metadata
Title
A layered algorithm for quantifier elimination from linear modular constraints
Authors
Ajith K. John
Supratik Chakraborty
Publication date
07-12-2016
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2016
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-016-0260-9

Premium Partner

    Image Credits