2026-08-10T17:38:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2790 2024-03-06T11:09:21Z ddc:004 open_access

A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra Abraham, Erika Corzilius, Florian Loup, Ulrich Sturm, Thomas SMT-solving Real Algebra Hybrid Systems Verification Synthesis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Erika Abraham and Florian Corzilius and Ulrich Loup and Thomas Sturm 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.10271.2 urn:nbn:de:0030-drops-27907 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.2 eng https://creativecommons.org/licenses/by/4.0/legalcode