Source: rumur Section: devel Priority: optional Maintainer: Matthew Fernandez Build-Depends: debhelper-compat (= 12), bison, cmake, flex, libfl-dev, libgmp-dev, python3, strace Standards-Version: 4.6.1.0 Homepage: https://github.com/Smattr/rumur Vcs-Git: https://github.com/Smattr/rumur.git -b packaging/debian Vcs-Browser: https://github.com/Smattr/rumur.git Rules-Requires-Root: no Package: rumur Architecture: any Depends: ${shlibs:Depends}, ${misc:Depends} Suggests: python3 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. Rumur comes with an optional wrapper script, rumur-run, that streamlines the process of generating a verifier, compiling it, and then running it. This wrapper requires Python.