We are currently offering two versions of Moped. Moped version 2
(previously known as nMoped) is a reimplementation of Moped on the basis of the
weighted PDS library and with some additional features (see below for details).
For backward compatibility, and also because the new version still lacks
a couple of features that the old version had, we are still offering
Moped version 1 for downloading (see below).
New developments will happen in the new version from now on, but we will
still attend to bugfixes in the old version.
There is now also a Java front-end for Moped, see the
jMoped page, and an Eclipse
plug-in for jMoped.
Moped is a model checker for pushdown systems.
Roughly speaking, the expressive power of pushdown systems is equivalent
to that of programs with (possibly recursive) procedures where all variables
have a finite data type. Moped can also process Boolean Programs and interact
with the SLAM toolkit.
Moped version 2
This new version of Moped has a new input language called Remopla,
a Promela-like language featuring explicit procedures. The
implementation is based on the WPDS library. Optionally, a
scheme for automatic abstraction can be employed, following the CEGAR
paradigm (CounterExample-Guided Abstraction Refinement).
The CEGAR process is described in detail in Stefan
Kiefer's Master thesis and in a TACAS'06
Currently, Moped version 2 allows for reachability checks.
LTL model checking is still offered by version 1 (see below).
- 29.07.2005: Version 1.0.0, initial release of the tool
- 16.05.2006: Version 1.1.0, new release with additional features and better trace generation
- 18.05.2006: Version 1.1.1, bugfix in bddTrace.c
- 31.05.2006: Version 1.1.2, bugfix in backwards reachability mode.
- 28.09.2006: Version 1.1.3, bugfix in bddDom.c.
- 15.12.2006: Version 1.2.0, some bugfixes and switches -B2 and -F2.
Moped version 1
This is the old version of Moped. It features both reachability and LTL
model checking. It can process pushdown systems and Boolean programs.
Moped is written and maintained by
Stefan Schwoon and