The Formal methods and Verification group of the Computer Science Department at ULB has developped over the time several (prototypical) tools in the field of computer-aided verification. The following list allows to navigate to their corresponding websites.

Tools for Petri nets and Well-structured transition systems


MIST implements several algorithms that solve the coverability problem for monotonic extensions of Petri nets. It implements, among others, the Expand, Enlarge and Check algorithm

>>> to MIST webpage


CSC implements an efficient algorithm to compute the coverability set of a Petri net

>>> to CSC webpage

Antichains based tools


Alaska solves the LTL model checking, LTL satisfiability and alternating automata emptiness problems


Alpaga solves imperfect information parity games.


Acacia solves the LTL realizability problem, and synthesis winning strategies.

Controller synthesis tools


Smacs (Symbolic Masked Controller Synthesis) is a tool aiming at the supervisory control of infinite state systems under partial observation.

Verification of Communicating Machines


McScM (Model Checker for Systems of Communicating fifo Machines) is a small framework for implementing model checking algorithms in the context of infinite state systems of the form “finite control plus infinite data”. McScM includes a suite of verification algorithms for the safety analysis of asynchronously fifo communicating processes that are an important model for TCP- or MPI-based distributed systems.

Verification of Timed Systems


MightyL is a tool to convert formulas written in the MITL logic into a set of timed automata, whose synchronous product accepts the language of the formula.

>>> to MightyL webpage


Interval Sharing Trees

Interval Sharing Trees are an efficient datastructure for representing constraints on intervals. They have been successfuly applied to several verification problems on Petri nets (see MIST and CSC above).

>>> to the IST library webpage

Lattice-Valued Binary Decision Diagrams

The LavaBDD library implements Lattice-Valued Binary Decision Diagrams, an efficient datastructure that allows to manipulates functions mapping valuations of Boolean variables to values taken from a finite distributive latttice. They have been successfully applied to the LTL satisfiability problem.

>>> to the LavaBDD webpage