Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
SZS | Contact | People | Teaching | Research | Publications | Tools | Institute | Department | Links
Institute of Formal Methods in Computer Science

Moped - A Model-Checker for Pushdown Systems
 

News

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.

Overview

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 paper. Currently, Moped version 2 allows for reachability checks. LTL model checking is still offered by version 1 (see below).

Downloads

Changes

  • 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.
  • Source code (Version 1.0.16, last changed: 10.09.2010)

Contact

Moped is written and maintained by Stefan Kiefer, Stefan Schwoon and Dejvuth Suwimonteerabuth.

Links

  
last change 15.10.2011 (mailto ss) |  © University of Stuttgart | legal notice