Sciweavers

Share
SPIN
2004
Springer

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

9 years 2 months ago
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.
Peter Leven, Tilman Mehler, Stefan Edelkamp
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SPIN
Authors Peter Leven, Tilman Mehler, Stefan Edelkamp
Comments (0)
books