Libdmc

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

'''Libdmc''' <ref>{{cite book|doi=10.1109/IPDPS.2007.370647 | isbn=978-1-4244-0909-9 | year=2007 | last1 = Hamez | first1 = Alexandre | last2 = Kordon | first2 = Fabrice | last3 = Thierry-Mieg | first3 = Yann| title=2007 IEEE International Parallel and Distributed Processing Symposium | chapter=IibDMC: A Library to Operate Efficient Distributed Model Checking | pages=1–8 | s2cid=12586847 }}</ref><ref>{{cite book|doi=10.1007/978-3-540-73094-1_29 | isbn=978-3-540-73093-4 | pages=495–504 | last1 = Hamez | first1 = Alexandre | last2 = Kordon | first2 = Fabrice | last3 = Thierry-Mieg | first3 = Yann | last4 = Legond-Aubry | first4 = Fabrice| title=Petri Nets and Other Models of Concurrency – ICATPN 2007 | chapter=DMCG: A Distributed Symbolic Model Checker Based on GreatSPN | series=Lecture Notes in Computer Science | volume=4546 | year=2007 }}</ref> is a library designed at the LIP6 <ref>[https://www.lip6.fr Accueil LIP6]</ref> 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 == {{reflist}}

Category:Model checkers