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.