Daniel Kroening (ETH Zentrum), Model Checking C++ Programs that use the STL

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.