License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10271.2
URN: urn:nbn:de:0030-drops-27907
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2790/
Go to the corresponding Portal

Abraham, Erika ; Corzilius, Florian ; Loup, Ulrich ; Sturm, Thomas

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

pdf-format:
10271.AbrahamErika.ExtAbstract.2790.pdf (0.3 MB)

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.

BibTeX - Entry

@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/opus/volltexte/2010/2790},
  URN =		{urn:nbn:de:0030-drops-27907},
  doi =		{10.4230/DagSemProc.10271.2},
  annote =	{Keywords: SMT-solving, Real Algebra, Hybrid Systems, Verification, Synthesis}
}

Keywords: SMT-solving, Real Algebra, Hybrid Systems, Verification, Synthesis
Collection: 10271 - Verification over discrete-continuous boundaries
Issue Date: 2010
Date of publication: 02.11.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI