Department of Information Technology

Algorithmic Program Verification Tools and Prototypes


We have developed several tools and prototypes. Some of these tools are listed below, feel free to contact us if you want some more information!

RMC: Regular Model Checking

RMC is a BDD-based tool for symbolic verification of systems againts LTL specification. The system can be for instance an unbounded number of finite state machines.

PFS: Parametrized Finite-state Systems

PFS is a prototype for the verification of parameterized systems. A parameterized system consists of an arbitrary number of identical finite-state machines running in parallel. For instance, many cache coherence protocols as well as mutual exclusion algorithms fit into this modeling framework.

UNDIP: UNbounded DIstributed Parameterized systems

UNDIP is a generalization of pfs to the case where: (i) the parameterized system is distributed, and (ii) where the variables, (shared, local to the processes or to the channels), can range over infinite domains. We use Difference bound matrices to manipulate the variables.

TBIS: Bismulation Minimization of Tree Automata

TBIS is a prototype for the minimization of non-deterministic bottom up tree automata modolu bisimulation. The algorithm used in the prototype is an extention of an algorithm by Paige and Tarjan that solves the coarsest stable
refinement problem to the domain of trees.

TPNS: Forward Reachability Analysis of Timed Petri Nets

TPNS is a prototype for the modeling and reachability analysis of timed petri nets.

Updated  2007-08-28 14:46:42 by Ahmed Rezine.