POEM (Partial Order Environment of Marseille) is a modular model checking tool built to support several input languages, several analysis and solving algorithms. POEM provides reusable code for some powerful partial order based model checking algorithms.

POEM consists of a set of modules interconnected : first, a model and a property are parsed by a frontend according to its language and represented with the global data structure GDS which plays the role of a bus for the three subsystems. core analyses and transforms the GDS structure in performing type checking, constant propagation, model transformation, transition generation including dependency analysis for partial order algorithms, etc. The result of this analysis is passed to the backend that implements solving algorithms to check the property. The core then transforms the findings (e.g. a trace) into an XML file that is readable by a GUI and allows the latter to visualise the found execution with a link to the source code.

A GUI (written in Java) has been developed with the following features: editor of model files with syntax colouring, configuration of POEM and user friendly display of results and error messages. The POEM executable itself is written in OCAML, a functional and imperative language. This choice was driven by useful features of this language like recursive types and the relative easy of rewriting which is used extensively throughout the program. Performance critical algorithms are delegated to external software written in C.