Miscellaneous CADP Resources

1. The VLPN (Very Large Petri Nets) Benchmark Suite

The VLPN benchmark suite is a collection of Nested-Unit Petri Nets (NUPNs) to be tackled by model checking tools.


2. The VLSAT (Very Large Boolean SATisfiability Problems) Benchmark Suites

The VLSAT benchmark suites are collections of logic formulas to be used in scientific experiments and software competitions. Three collections are available at the moment:


3. The VLTS (Very Large Transition Systems) Benchmark Suite

The VLTS benchmark suite is a collection of Labelled Transition Systems. It is designed to be a reference criterion for scientific assessment of algorithms and tools operating on large graphs.

The VLTS benchmark suite was a joint project of CWI/SEN2 and INRIA/VASY.



4. Libraries of Specification Patterns in Temporal Logics

Temporal logics and mu-calculus is not always easy, especially for novice users. This can be solved, at least partially, by the use of predefined libraries. Two such libraries are provided below:

These two libraries have been developed by Radu Mateescu (INRIA/VASY).


5. A Catalog of Tools for the Quantitative Zoo

This catalog lists a number of models, logics, and tools developed for modelling and verifying complex systems, the behaviour of which combines discrete aspects (namely, states and transitions) and continuous features (e.g., time, delays, probabilities, continuous laws, etc.).


6. Enhanced Version of the Memtime Utility

Memtime is a command-line tool for measuring the CPU and memory consumption of a program. The INRIA/VASY and INRIA/CONVECS teams provide enhanced versions of Memtime that are used daily for the development of the CADP toolbox: Related sites:
Version 1.29 last updated on 2021/08/26 18:00:45

Back to the CADP Home Page