State Exploring Assembly Model Checker for the verification of native C++-programs!
StEAM-XXL is a development by the Bugfinder project group which can solve bigger problems by storing information on hard disk.
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.
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.
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.
StEAM is developed at the LS5 at University of Dortmund.
StEAM is extended during a project group at Chair for Programming Languages, University of Dortmund. The Progect group included :
Tilman Mehler has developed StEAM around the Internet C++ Virtual Machine as his dissertation.