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
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
CSC
CSC implements an efficient algorithm to compute the coverability set of a Petri net
Antichains based tools
Alaska
Alaska solves the LTL model checking, LTL satisfiability and alternating automata emptiness problems
Alpaga
Alpaga solves imperfect information parity games.
Acacia
Acacia solves the LTL realizability problem, and synthesis winning strategies.
Controller synthesis tools
Smacs
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
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
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.
Libraries
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).
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.