ITP: rumur -- model checker for the Murphi language
Package: wnpp
Severity: wishlist
Owner: Matthew Fernandez <matthew.fernandez@gmail.com>
* Package name : rumur
Version : 2019.01.12
Upstream Author : Matthew Fernandez <matthew.fernandez@gmail.com>
* URL : https://github.com/Smattr/rumur
* License : The Unlicense
Programming Lang: C, C++, Python
Description : model checker for the Murphi language
Rumur is a model checker for use in the formal verification of finite state
machines specified in the Murphi modelling language. It is based on a previous
tool, CMurphi, and attempts to provide an approximate drop-in replacement for
CMurphi.
Rumur works by reading an input file describing a collection of state variables
and transition rules, from which it generates a C program to verify safety and
security properties of this state machine. The generated verifier works by
exhaustively exploring the state space, checking for violation of invariants or
deadlocks.
In comparison to CMurphi, Rumur generates a verifier that runs significantly
faster and uses less memory on large input problems.
The Murphi modelling language has been used extensively for hardware
verification, in particular for analysing cache coherence protocols. Rumur is
able to improve existing users’ work flow by decreasing the time to check these
models. I am not aware of any other Debian packages that provide this
functionality; existing CMurphi users generally build the tool from source.
I am the sole developer and maintainer of this tool and intend to be its
Debian maintainer as well. I have not packaged or maintained a tool for Debian
before, so I am looking for a sponsor.
Reply to: