Directed error detection in C++ with the assembly-level model checker StEAM. Most approaches for model checking software are based on the generation 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 StEAM (State Exploring Assembly Model Checker) can successfully enhance the detection of deadlocks and assertion violations.

References in zbMATH (referenced in 6 articles , 1 standard article )

Showing results 1 to 6 of 6.
Sorted by year (citations)

  1. Edelkamp, Stefan; Kellershoff, Mark; Sulewski, Damian: Program model checking via action planning (2011) ioport
  2. Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
  3. Weber, Michael: An embeddable virtual machine for state space generation (2010) ioport
  4. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009) ioport
  5. Balakrishnan, G.; Reps, T.; Kidd, N.; Lal, A.; Lim, J.; Melski, D.; Gruian, R.; Yong, S.; Chen, C.-H.; Teitelbaum, T.: Model checking x86 executables with CodeSurfer/x86 and WPDS++ (2005)
  6. Leven, Peter; Mehler, Tilman; Edelkamp, Stefan: Directed error detection in C++ with the assembly-level model checker StEAM (2004)