Daniel Kroening
*Assistant Professor, Computer Systems Institute*

Model Checking C++ Programs that use the STL

Abstract:

Motivated by the need for scalable symbolic reasoning methodologies
aimed at systems biology, as well as the novel opportunities made possible by
powerful hybrid automata models of biochemical networks, we have embarked upon
the Algorithmic Algebraic Model Checking (AAMC) project that combines symbolic
computation with model checking to analyze biochemical systems. Briefly, AAMC
aims to identify a decidable (ultimately, practical) component of a theory for
systems biology by examining the connections between semi-algebraic hybrid automata,
modal logic, computability and systems biology, starting with a characterization
based on Semi-Algebraic Hybrid Automata.

In Semi-Algebraic Hybrid Automata, the continuous dynamics and discrete jump
conditions are defined by first-order formulæ whose terms are polynomials
over the reals. Consequently, they can exploit a series of real algebraic techniques,
based on Tarski's result on the decidability of real quantifier elimination,
to study the possible evolutions of the system entirely symbolically. Beyond
decidability of Timed Computation Tree Logic (TCTL), we studied Semi-Algebraic
Constant Reset Automata and Independent Dynamics Automata whose resets were
constrained to be constant or identity, thus providing a suitable generalization
of O-minimal systems without sacrificing decidability.

Short Bio:

Verifying
general properties of full-featured C++ code is beyond the scope of current
model checking and predicate abstraction techniques. However, just as Microsoft's
SLAM project concentrates on verifying the usage of well-defined APIs in device
drivers written in C, the restrictions the C++ Standard makes on the usage of
the C++ Standard Template Library (STL) can be verified using a specialized
form of counterexample-guided abstraction refinement. We a flexible and easily
extensible predicate abstraction-based approach to the verification of STL usage.
We formalize the semantics of the STL by means of a Hoare-style axiomatization.
The verification requires an operational model, for which we show that it conservatively
approximates the semantics given by the standard.

Motivated by the need for scalable symbolic reasoning methodologies aimed at
systems biology, as well as the novel opportunities made possible by powerful
hybrid automata models of biochemical networks, we have embarked upon the Algorithmic
Algebraic Model Checking (AAMC) project that combines symbolic computation with
model checking to analyze biochemical systems. Briefly, AAMC aims to identify
a decidable (ultimately, practical) component of a theory for systems biology
by examining the connections between semi-algebraic hybrid automata, modal logic,
computability and systems biology, starting with a characterization based on
Semi-Algebraic Hybrid Automata.

In Semi-Algebraic Hybrid Automata, the continuous dynamics and discrete jump
conditions are defined by first-order formulæ whose terms are polynomials
over the reals. Consequently, they can exploit a series of real algebraic techniques,
based on Tarski's result on the decidability of real quantifier elimination,
to study the possible evolutions of the system entirely symbolically. Beyond
decidability of Timed Computation Tree Logic (TCTL), we studied Semi-Algebraic
Constant Reset Automata and Independent Dynamics Automata whose resets were
constrained to be constant or identity, thus providing a suitable generalization
of O-minimal systems without sacrificing decidability.