{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article2778","name":"A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra","abstract":"There are several methods for the synthesis and analysis of hybrid\r\nsystems that require efficient algorithms and tools for satisfiability\r\nchecking. For analysis, e.g., bounded model checking describes\r\ncounterexamples of a fixed length by logical formulas, whose\r\nsatisfiability corresponds to the existence of such a counterexample.\r\nAs an example for parameter synthesis, we can state the correctness of\r\na parameterized system by a logical formula; the solution set of\r\nthe formula gives us possible safe instances of the parameters.\r\n\r\nFor discrete systems, which can be described by propositional logic\r\nformulas, SAT-solvers can be used for the satisfiability checks. For\r\nhybrid systems, having mixed discrete-continuous behavior, SMT-solvers\r\nare needed. SMT-solving extends SAT with theories, and has its main\r\nfocus on linear arithmetic, which is sufficient to handle, e.g.,\r\nlinear hybrid systems. However, there are only few solvers for\r\nmore expressive but still decidable logics like the\r\nfirst-order theory of the reals with addition and multiplication --\r\nreal algebra. Since the synthesis and analysis of non-linear\r\nhybrid systems requires such a powerful logic, we need efficient\r\nSMT-solvers for real algebra. Our goal is to develop such an\r\nSMT-solver for the real algebra, which is both complete and\r\nefficient.","keywords":["SMT-solving","Real Algebra","Hybrid Systems","Verification","Synthesis"],"author":[{"@type":"Person","name":"Abraham, Erika","givenName":"Erika","familyName":"Abraham"},{"@type":"Person","name":"Corzilius, Florian","givenName":"Florian","familyName":"Corzilius"},{"@type":"Person","name":"Loup, Ulrich","givenName":"Ulrich","familyName":"Loup"},{"@type":"Person","name":"Sturm, Thomas","givenName":"Thomas","familyName":"Sturm"}],"position":2,"pageStart":1,"pageEnd":9,"dateCreated":"2010-11-02","datePublished":"2010-11-02","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Abraham, Erika","givenName":"Erika","familyName":"Abraham"},{"@type":"Person","name":"Corzilius, Florian","givenName":"Florian","familyName":"Corzilius"},{"@type":"Person","name":"Loup, Ulrich","givenName":"Ulrich","familyName":"Loup"},{"@type":"Person","name":"Sturm, Thomas","givenName":"Thomas","familyName":"Sturm"}],"copyrightYear":"2010","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.10271.2","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume814","volumeNumber":10271,"name":"Dagstuhl Seminar Proceedings, Volume 10271","dateCreated":"2010-11-02","datePublished":"2010-11-02","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article2778","isPartOf":{"@type":"Periodical","@id":"#series119","name":"Dagstuhl Seminar Proceedings","issn":"1862-4405","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume814"}}}