Technical Report No. 193 - Abstract

Tilman Mehler, Peter Leven
Introduction to StEAM - An Assembly-Level Software Model Checker

\begin{abstract} Model checking techniques have been used successfully for the exploration of state-based systems to search systematically for errors. As a recent trend, model checking was applied for the verification of software. Most of the current approaches are based on the (semi-)automatic generation of an abstract model from the source code. Such an abstraction may not correctly reflect the behavior of the actual program. This means, the abstract model may contain errors which are not present in the actual program and vice versa. Some newer approaches - such as the Java model checker JPF - avoid this problem, by checking the actual program instead of an abstract model. In our own work we focus on the mainly used programming language C++. The usage of a virtual machine for C++ and our extension to multi threading allows platform independent model checking of thread based C++-programs. First examples show, that our system \steam\footnote{State Exploring Assembly Model Checker} can successfully be used to detect deadlocks and assertion violations. \end{abstract}