2 Search Results for "Sturm, Thomas"

Document
DOI: 10.4230/DagRep.5.11.71
Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471)

Authors: Erika Ábrahám, Pascal Fontaine, Thomas Sturm, and Dongming Wang

Published in: Dagstuhl Reports, Volume 5, Issue 11 (2016)

Abstract
The seminar focused on satisfiability checking for combinations of first-order logic and subclasses thereof with arithmetic theories in a very liberal sense, also covering quantifiers and parameters. It gathered members of the two communities of symbolic computation (or computer algebra) and satisfiability checking (including satisfiability modulo theories). Up-to-now, these two communities have been working quite independently. We are confident that the seminar will initiate cross-fertilization of both fields and bring improvements for both satisfiability checking and symbolic computation, and for their applications.
Cite as

Erika Ábrahám, Pascal Fontaine, Thomas Sturm, and Dongming Wang. Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). In Dagstuhl Reports, Volume 5, Issue 11, pp. 71-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{abraham_et_al:DagRep.5.11.71,
  author =	{\'{A}brah\'{a}m, Erika and Fontaine, Pascal and Sturm, Thomas and Wang, Dongming},
  title =	{{Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471)}},
  pages =	{71--89},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2016},
  volume =	{5},
  number =	{11},
  editor =	{\'{A}brah\'{a}m, Erika and Fontaine, Pascal and Sturm, Thomas and Wang, Dongming},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.11.71},
  URN =		{urn:nbn:de:0030-drops-57657},
  doi =		{10.4230/DagRep.5.11.71},
  annote =	{Keywords: algorithmic algebra, arithmetic, automated reasoning, decision procedures, quantifier elimination, satisfiability checking, SMT solving, symbolic comp}
}
Document
DOI: 10.4230/DagSemProc.10271.2
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-dev.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}
}
  • Refine by Author
  • 2 Sturm, Thomas
  • 1 Abraham, Erika
  • 1 Corzilius, Florian
  • 1 Fontaine, Pascal
  • 1 Loup, Ulrich
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 Hybrid Systems
  • 1 Real Algebra
  • 1 SMT solving
  • 1 SMT-solving
  • 1 Synthesis
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2010
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact