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
apt install rumurpkg install rumurThanks to yuri@FreeBSD for packaging.
pacman -S rumurThanks to Qirui Wang (wangqr) for packaging.
First you will need to have the following dependencies installed:
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.outCompilation 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.
If you are migrating from CMurphi, you can read a comparison between the two model checkers at doc/vs-cmurphi.rst.
Everything in this repository is in the public domain, under the terms of the Unlicense. For the full text, see LICENSE.