Directed Error Detection in C++ with the Assembly-Level Model Checker StEAM

Most approaches for model checking software are based on ration of abstract models from source code, which may greatly reduce the search space, but may also introduce errors that are not present in the actual program. In this paper, we propose a new model checker for the verification of native c++-programs. To allow platform independent model checking of the object code for concurrent programs, we have extended an existing virtual machine for c++ to include multi-threading and different exploration algorithms on a dynamic state description. The error reporting capabilities and the lengths of counter-examples are improved by using heuristic estimator functions and state space compaction techniques that additionally reduce the exploration efforts. The evaluation of four scalable simple example problems shows that our system StEAM3 can successfully enhance the detection of deadlocks and assertion violations.

• Type: Conference
• Year: 2004
• Where: SPIN
• Authors: Peter Leven, Tilman Mehler, Stefan Edelkamp
• Keywords: Independent Model Checking, Model Checking, Model Checking Software, SPIN 2004, Theoretical Computer Science