Libdmc
 |
This article is an orphan, as few or no other articles link to it. Please introduce links to this page from related articles; suggestions may be available. (February 2009) |
| Developer(s) | Alexandre Hamez |
|---|---|
| Operating system | Posix Systems |
| Type | Model checking |
Libdmc [1][2] is a library designed at the LIP6 [3] laboratory. Its goal is to ease the distribution of existing model checkers. It has also been designed to provide the most generic interfaces, without sacrificing performance, thanks to the C++ language.
Model checking offers a way to automatically prove that a modeled system behavior is correct by verifying properties. However, it suffers from the so-called state space explosion problem, caused by an intensive use of memory. Many solutions have been proposed to overcome this problem (e.g. symbolic representations with decisions diagrams - like BDD) but these methods can rapidly lead to an 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, so the approach of libdmc is to give a framework in order to construct a model checker.
[edit] References
  |
This bioinformatics-related article is a stub. You can help Wikipedia by expanding it. |
