StEAM - State Exploring Assembly Model Checker

StEAM-XXL - StEAM with externalization


State Exploring Assembly Model Checker for the verification of native C++-programs!

What is StEAM / StEAM-XXL?

StEAM is a model checker for C++. It detects deadlocks, segmentation faults, out of range variables and non-terminating loops.

StEAM-XXL is a development by the Bugfinder project group which can solve bigger problems by storing information on hard disk.

How does it work?

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. To solve this problem, StEAM performs the error search on machine-code compiled from a C++ source.

How is it done?

We have extended the existing virtual machine for C++, Internet C++ Virtual Machine 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. StEAM can successfully enhance the detection of deadlocks and assertion violations. To learn more about StEAM, refer to the documentation page.

Download

You can download StEAM from the download section. Currently StEAM is only available for Linux, as source, Debian and RPM package. You can learn more about porting and packages in the download section.

Developing process

StEAM is developed at the LS5 at University of Dortmund.

Current Developers:

Project group participants

StEAM is extended during a project group at Chair for Programming Languages, University of Dortmund. The Progect group included :

First appearance

Tilman Mehler has developed StEAM around the Internet C++ Virtual Machine as his dissertation.