DROPS

Document

A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra

Authors: Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract

There are several methods for the synthesis and analysis of hybrid systems that require efficient algorithms and tools for satisfiability checking. For analysis, e.g., bounded model checking describes counterexamples of a fixed length by logical formulas, whose satisfiability corresponds to the existence of such a counterexample. As an example for parameter synthesis, we can state the correctness of a parameterized system by a logical formula; the solution set of the formula gives us possible safe instances of the parameters. For discrete systems, which can be described by propositional logic formulas, SAT-solvers can be used for the satisfiability checks. For hybrid systems, having mixed discrete-continuous behavior, SMT-solvers are needed. SMT-solving extends SAT with theories, and has its main focus on linear arithmetic, which is sufficient to handle, e.g., linear hybrid systems. However, there are only few solvers for more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication -- real algebra. Since the synthesis and analysis of non-linear hybrid systems requires such a powerful logic, we need efficient SMT-solvers for real algebra. Our goal is to develop such an SMT-solver for the real algebra, which is both complete and efficient.

Cite as

Erika Abraham, Florian Corzilius, Ulrich Loup, and Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{abraham_et_al:DagSemProc.10271.2,
  author =	{Abraham, Erika and Corzilius, Florian and Loup, Ulrich and Sturm, Thomas},
  title =	{{A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.2},
  URN =		{urn:nbn:de:0030-drops-27907},
  doi =		{10.4230/DagSemProc.10271.2},
  annote =	{Keywords: SMT-solving, Real Algebra, Hybrid Systems, Verification, Synthesis}
}

Document

DOI: 10.4230/DagSemProc.09461.3

SMT-Solving for the First-Order Theory of the Reals

Authors: Erika Abraham and Ulrich Loup

Published in: Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010)

Abstract

SAT-solving is a highly actual research area with increasing success and plenty of industrial applications. SMT-solving, extending SAT with theories, has its main focus on linear real constrains. However, there are only few solvers going further to more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication. The main requests on theory solvers that must be fulfilled for their efficient embedding into an SMT solver are (a) incrementality, (b) the efficient computation of minimal infeasible subsets, and (c) the support of backtracking. For the first-order theory of the reals we are not aware of any solver offering those functionalities. In this work we address the possibilities to extend existing theory solving algorithms to come up with a theory solver suited for SMT.

Cite as

Erika Abraham and Ulrich Loup. SMT-Solving for the First-Order Theory of the Reals. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{abraham_et_al:DagSemProc.09461.3,
  author =	{Abraham, Erika and Loup, Ulrich},
  title =	{{SMT-Solving for the First-Order Theory of the Reals}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.3},
  URN =		{urn:nbn:de:0030-drops-25081},
  doi =		{10.4230/DagSemProc.09461.3},
  annote =	{Keywords: SMT-solving, first-order theory of the reals, verification}
}

Search Results

Documents authored by Loup, Ulrich

A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra

Abstract

Cite as

SMT-Solving for the First-Order Theory of the Reals

Abstract

Cite as

Thanks for your feedback!

Could not send message