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.

Building from Source

First you will need to have the following dependencies installed:

Either GCC or Clang
Bison
CMake
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;
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.