Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleReal world verification.
Author(s) Andre Platzer, Jan-David Quesel, Philipp Rümmer
TypeBook, Chapter in Book, Conference Proceeding
AbstractScalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gröbner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gröbner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.
KeywordsReal-closed fields, decision procedures, hybrid systems
URL http://link.springer.com/chapter/10.1007%2F978-3-642-02959-2_35
PublisherBerlin: Springer
Translation No
Refereed No