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
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
- 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.