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 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 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 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 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 is a prototype for the modeling and reachability analysis of timed petri nets.