Static POR of Message-Passing Protocols.

MP-Basset is a model checker for message-passing systems. It extends the Basset model checker with quorum transitions, i.e., atomic events consuming multiple messages. MP-Basset supports Partial-Order Reduction (POR) for better scalability of model checking complex message-passing protocols.


Release of MP-Basset extension with new optimization called Decompasition-Based Stateful Search (DBBS). The optimization consists of the following features:

  • Selective push-on-stack for time-efficient backtracking.
  • Selective hashing for more efficient state matching.
  • New JPF core version (6.0).

The source code of DBSS/MP-Basset is available for download.


MP-Basset supports dynamic Partial-Order Reductions (POR) via Basset, and implements a new static POR algorithm called Local POR (LPOR) [2]. Die new version of MP-Basset also supports MP-State, which is an improvement of explicit-state software model checking of message passing programs.

A short user guide of MP-Basset can be found in [1].


Péter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri, “Efficient Model Checking of Fault-Tolerant Distributed Protocols”, Proc. of the IEEE Int’l Conf. on Dependable Systems and Networks (DSN-DCCS), 2011


Péter Bokor, Johannes Kinder, Marco Serafini and Neeraj Suri, “Supporting Domain-Specific State Space Reductions through Local Partial-Order Reduction”, Proc. of the 26th IEEE/ACM Int’l Conf. on Automated Software Engineering (ASE), pp. 113-122, 20111.

Download & Installation

The complete source code of MP-Basset is available here. The new version of MP-Basset is integrated with the latest JPF core and includes our new technique MP-State.

MP-Basset includes Java Pathfinder (the model checker engine utilized by Basset, and, in turn, MP-Basset) and a Java-based open library implementation of LPOR.

MP-Basset can be installed similar to Basset.

MP-Basset runs from the command line. You can run your first MP-Basset application using the following simple script (MPBasset).

For example, the following command starts MP-Basset with LPOR for the model of the Paxos consensus protocol with 3 acceptor processes.

./MPbasset +fw.spor=1 3


Example message-passing protocols written in MP, the input language of MP-Basset, can be found in the MP-Basset distribution (/jpf-actor/src/examples/).

The following examples are available:

  • Paxos consensus: /jpf-actor/src/examples/paxos/
  • Echo multicast: /jpf-actor/src/examples/multicast/
  • Regular register: /jpf-actor/src/examples/register/
  • Zab atomic broadcast: /jpf-actor/src/examples/zab/