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

20-04-2016

A search-based procedure for nonlinear real arithmetic

Authors: Ashish Tiwari, Patrick Lincoln

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

We present a new procedure for testing satisfiability (over the reals) of a conjunction of polynomial equations. There are three possible return values for our procedure: it either returns a model for the input formula, or it says that the input is unsatisfiable, or it fails because the applicability condition for the procedure, called the eigen-condition, is violated. For the class of constraints where the eigen-condition holds, our procedure is a decision procedure. We describe satisfiability-preserving transformations that can potentially convert problems into a form where eigen-condition holds. We experimentally evaluate the procedure on constraints generated by template-based verification and synthesis procedures.
previous article From invariant checking to invariant inference using randomized search
next article Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components

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.
Akbarpour B, Paulson LC (2010) MetiTarski: An automatic theorem prover for real-valued special functions. J Autom Reason 44(3):175–205MathSciNetCrossRefMATH
2.
Bachmair L, Ganzinger H (1994) Buchberger’s algorithm: a constraint-based completion procedure. In: Proceedings of 1st international conference constraints in computational logic, LNCS 845, Springer, pp 285–301
3.
4.
5.
Buchberger B (1983) A critical-pair completion algorithm for finitely generated ideals in rings. In: Proceedings of logic and machines: decision problems and complexity, LNCS, vol. 171, pp 137–161
6.
Cheng CH, Ruess H, Shankar N (2013) JBernstein: a validity checker for generalized polynomial constraints. In: Proceedings of 25th international conference computer aided verification, CAV, vol. LNCS 8044, Springer, pp 656–661
7.
Cheng CH, Shankar N, Ruess H, Bensalem S (2013) EFSMT: a logical framework for cyber-physical systems. CoRR abs/1306.3456
8.
Collins GE (1975) Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Proceedings of 2nd GI Conference on Automata Theory and Formal Languages, LNCS, Springer, vol. 33, pp 134–183
9.
10.
Colon M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: Computer-Aided Verification (CAV), LNCS, Springer-Verlag, vol. 2725, pp 420–433
11.
12.
13.
14.
Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3–4):209–236MATH
15.
Ganzinger H, Hagen G, Nieuwenhuis R, Oliveras A, Tinelli C (2004) DPLL(T): fast decision procedures. In: Proceedings of 16th International Conference on Computer Aided Verification, CAV 2004, LNCS, Springer, vol 3114, pp 175–188
16.
Gao S, Avigad J, Clarke EM (2012) \(\delta \)-complete decisionprocedures for satisfiability over the reals. In: Proceedings 6th International Conference Automated Reasoning, IJCAR, LNCS 7364, pp 286–300
17.
Gao S, Kong S, Clarke EM (2013) dReal: An SMT solver for nonlinear theories over the reals. In: Proceedings of 24th International Conference on Automated Deduction, CADE, LNCS 7898, Springer, pp 208–214
18.
19.
Gulwani S, Jha S, Tiwari A, Venkatesan R (2011) Synthesis of loop-free programs. In: Proceedings of ACM Conference on Prgramming Language Designing and Implementation of PLDI, pp 62–73
20.
Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: Proceedings of ACM Conference on Prgramming Language Design and implementaion, PLDI, pp 281–292
21.
Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Proceedings of 20th International Conference on Computer Aided Verification, CAV 2008, LNCS, vol. 5123, pp 190–203. Springer. July 7–14, 2008, Princeton, NJ
22.
Hong H (1990) An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of ISAAC 90, pp 261–264
23.
24.
Iwane H, Yanami H, Anai H (2011) An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems. In: Proceedings of International Workshop on Symbolic Numeric Computation, SNC, pp 168–177. ACM
25.
Jovanovic D, de Moura LM (2012) Solving non-linear arithmetic. In: Proceedings of 6th International Conference Automated Reasoning, IJCAR, LNCS 7364, Springer, pp 339–354
26.
27.
Leike J, Tiwari A (2014) Synthesis for polynomial lasso programs. In: Proceedings of VMCAI, LNCS 8318, pp 454–472
28.
Loup U, Scheibler K, Corzilius F, Ábrahám E, Becker B (2013) A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Proceedings of 24th International Conference on Automated Deduction, CADE, LNCS 7898, Springer, pp 193–207
29.
Matringe N, Moura AV, Rebiha R (2010) Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Proceedings of 17th International Static Analysis Symposium, SAS, Springer, vol. LNCS 6337, pp 373–389
30.
31.
32.
Rebiha R, Matringe N, Moura AV (2012) Transcendental inductive invariants generation for non-linear differential and hybrid systems. In: Proceedings of Hybrid System: Computation and Control, HSCC, pp 25–34. ACM
33.
Renegar J (1992) On the computational complexity and geometry of the first-order theory of the reals. J Symb Comput 13(3):255–352MathSciNetCrossRefMATH
34.
Sankaranarayanan S, Sipma H, Manna Z (2004) Constructing invariants for hybrid systems. In: R. Alur, G.J. Pappas (eds.) Hybrid systems: computation and control, HSCC 2004, Lecture Notes in Computer Science, vol. 2993, pp 539–554. Springer
35.
Sankaranarayanan S, Sipma HB, Manna Z (2008) Constructing invariants for hybrid systems. Formal Methods Syst Des 32(1):25–55CrossRefMATH
36.
37.
Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. STTT 15(5–6):497–518CrossRef
38.
Stengle G (1974) A Nullstellensatz and a Positivstellensatz insemialgebraic geometry. Math Ann 207
39.
Sturm T, Tiwari A (2011) Verification and synthesis using real quantifier elimination. In: Proceedings of International Symposium on Symbolic and Algebraic Computation , ISSAC, pp 329–336. ACM
40.
Taly A, Gulwani S, Tiwari A (2009) Synthesizing switching logic using constraint solving. In: Proc. 10th Intl. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI, LNCS, Springer, vol. 5403, pp 305–319
41.
Tarski A (1948) A decision method for elementary algebra and geometry, 2nd edn. University of California Press, BerkeleyMATH
42.
Tiwari A (2005) An algebraic approach for the unsatisfiability of nonlinear constraints. In: Computer Science Logic, 14th Annual Conference, CSL 2005, LNCS, Springer, vol. 3634, pp 248–262
43.
Tiwari A, Khanna G (2004) Nonlinear Systems: Approximating reach sets. In: Proceedings of 7th International Workshop on Hybrid Systems: Computation and Control, HSCC 2004, LNCS, Springer, vol. 2993, pp 600–614
44.
Tiwari A, Lincoln P (2014) A nonlinear real arithmetic fragment. In: Proceedings on Computer Aided Verification CAV, LNCS, Springer, vol. 8559, pp 729–736
Metadata
Title
A search-based procedure for nonlinear real arithmetic
Authors
Ashish Tiwari
Patrick Lincoln
Publication date
20-04-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-0245-8

Other articles of this Issue 3/2016

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

OriginalPaper

An efficient SMT solver for string constraints

OriginalPaper

From invariant checking to invariant inference using randomized search

OriginalPaper

The spirit of ghost code

OriginalPaper

SMT-based model checking for recursive programs

OriginalPaper

Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components

EditorialNotes

2014 CAV award announcement

Premium Partner

    Image Credits