Libdmc
From Wikipedia, the free encyclopedia
| libdmc | |
| Developer: | Alexandre Hamez |
|---|---|
| OS: | Posix Systems |
| Use: | Model checking |
| Website: | https://srcdev..lip6.fr/svn/research/ahamez |
Model checking offers a way to automatically prove that a modeled system behavior is correct by verifying properties. However, it suffers of the so-called state space explosion problem, caused by an intensive use of memory. Many solutions have been proposed to overcome this problem like symbolic representations with decisions diagrams. But these methods can rapidly lead to a unacceptable time consumption.
Distributed model checking is a way to overcome both memory and time consumptions by using aggregated resources of a dedicated cluster. However, re-writing an entire model checker is a difficult task
libdmc is a library designed by Alexandre Hamez. It's goal is to ease the distribution of existing model checkers. It also has been designed to provide the most generic interfaces, without sacrificing to performances, thanks to the C++ language.
