Libdmc

Infobox Software
name = libdmc
developer = Alexandre Hamez
latest_release_version =
latest_release_date =
operating_system = Posix Systems
genre = Model checking

Libdmc [ [http://dx.doi.org/10.1109/IPDPS.2007.370647 IEEE Xplore# Wrapper Result ] ] [ [http://dx.doi.org/10.1007/978-3-540-73094-1_29 SpringerLink Home - Main ] ] is a library designed at the LIP6 [ [http://www.lip6.fr Accueil LIP6 ] ] 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.

References