Regular Model Checking

Regular Model Checking

Regular Model Checking is a framework for unified verification of infinite-state systems based on automata theory. It represents states using words over a finite alphabet and sets of states using finite automata. Recently, these techniques have also been applied to finite trees and we hope to generalize these techniques to other kinds of structures such as graphs. For an introduction to Regular Model Checking, you can look at the Licentiate Thesis of Marcus Nilsson.

In the Software section you will find the following packages, licensed under GPL:

  • Meta package for BDDs. The package gbdd implements an abstraction layer on top of BDDs. This allows several BDD implementation to be used under one API.
  • Implementation of finite-state automata The package gautomata implements finite-state automata with BDDs as edges.
  • Implementation of Regular Model Checking An application that can find models of LTL(MSO) formulas, built on top of gautomata and gbdd.


  • 2004-09-09 rmc 0.3 released. Acceleration of disjuncts is now supported, allowing safety for Szymanski to be verified again. Run rmc --acceleration=tc /usr/share/doc/rmc-0.3/examples/szymanski.l
  • 2004-08-12 New versions of Regular Model Checking software released. The old modules regrel and regeval are gone and replaced by a general rmc package that is built on top of gbdd and gautomata. Now compiled under Fedore Core 2.
  • 2004-05-11 Source tarballs for CVS snapshots added.
  • 2004-04-05 yum repository for CVS snapshots available. Compiled with RedHat Fedore Core 1
  • 2003-03-14 New versions of software released. Now compiled with RedHat 9.0.
  • 2003-02-11 Website reorganized
  • 2003-02-04 Documentation snapshots Added snapshots of documentation.
  • 2003-02-04 Version 0.8 Version 0.8 of GBDD released.
  • 2003-02-03 Version 0.7 Version 0.7 of GBDD released.
  • 2002-11-13 Snapshots Daily CVS snapshots added
  • 2002-10-14 Version 0.5 Version 0.5 of all tools released.
  • 2002-09-29 Bugzilla Added public bugzilla database for bugs.
  • 2002-07-19 IF support Added compilation with IF-support which gives a program if2rmc, a prototype filter from IF.

Last changed: Monday, 12-Aug-2013 16:55:04 CEST