Rumur

Rumur is a model checker, a formal verification tool for proving safety and security properties of systems represented as state machines. It is based on a previous tool, CMurphi, and intended to be close to a drop-in replacement. Rumur takes the same input format as CMurphi, the Murphi modelling language, with some extensions and generates a C program that implements a verifier.

A more extended introduction is available in doc/introduction.rst

Quickstart

Installation on Ubuntu or Debian

 apt install rumur

Installation on FreeBSD

 pkg install rumur

Thanks to yuri@FreeBSD for packaging.

Installation on Arch Linux

 pacman -S rumur

Thanks to Qirui Wang (wangqr) for packaging.

Building from Source

First you will need to have the following dependencies installed:

• Either GCC or Clang
• Bison
• CMake ≥ 3.5
• Flex
• Libgmp
• Python ≥ 3.4

Then:

 # Download Rumur
 git clone https://github.com/Smattr/rumur
 cd rumur
 
 # Configure and compile
 cmake -B build -S .
 cmake --build build
 cmake --install build
 
 # Generate a checker
 rumur my-model.m --output my-model.c
 
 # Compile the checker (also pass -mcx16 if using GCC on x86-64)
 cc -std=c11 -march=native -O3 my-model.c -lpthread
 
 # Run the checker
 ./a.out

Compilation produces several artefacts including the rumur binary itself:

• rumur: Tool for translating a Murphi model into a program that implements a checker;
• murphi-format: Reformatter for Murphi models;
• murphi2c: Tool for translating a Murphi model into C code for use in a simulator;
• murphi2murphi: A preprocessor for Murphi models;
• murphi2smv: Tool for translating a Murphi model into NuSMV input;
• murphi2uclid: Tool for translating a Murphi model into Uclid5 input;
• murphi2xml: Tool for emitting an XML representation of a Murphi model’s Abstract Syntax Tree;
• librumur.a: A library for building your own Murphi model tools; and
• include/rumur/: The API for the above library.

Comparison with CMurphi

If you are migrating from CMurphi, you can read a comparison between the two model checkers at doc/vs-cmurphi.rst.

Legal

Everything in this repository is in the public domain, under the terms of the Unlicense. For the full text, see LICENSE.