Real world verification

Scalable 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.

@inproceedings{DBLP:conf/cade/PlatzerQR09,
	pdf = {pub/rwv.pdf},
	slides = {pub/rwv-slides.pdf},
	study = {pub/rwv-examples.zip},
	TR = {DBLP:conf/cade/PlatzerQR09:TR},
	author = {['André Platzer', 'Jan-David Quesel', 'Philipp Rümmer']},
	title = {Real World Verification},
	booktitle = {CADE},
	longbooktitle = {International Conference on Automated
               Deduction, CADE-22, Montreal, Canada,
               Proceedings},
	year = {2009},
	pages = {485-501},
	editor = {['Renate A. Schmidt']},
	publisher = {Springer},
	series = {LNCS},
	volume = {5663},
	doi = {10.1007/978-3-642-02959-2_35},
	keywords = {real-closed fields, decision procedures,
               hybrid systems, software verification},
	abstract = {
    Scalable 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.}
}