What is CADP?
Home Page Tools Overview Current Status Recent Changes
Installation
How to obtain CADP? Usage Statistics
Documentation
FAQ Tutorials Publications Manual Pages Demo Examples Wikipedia
CADP Community
Newsletters Education & Training Case Studies Research Tools
CADP Resources
VLSAT Benchmarks VLTS Benchmarks Other Resources
About CADP
Contributors

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:

• The VLSAT-1 benchmark suite: a collection of SAT formulas dedicated to model counting.

• The VLSAT-2 benchmark suite: a collection of SAT formulas dedicated to SAT solving.

• The VLSAT-3 benchmark suite: a collection of SMT formulas dedicated to SMT solving.

---

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:

• Library of usual properties expressed in the ACTL temporal logic

• Library of usual properties expressed in the regular alternation-free mu-calculus language accepted by the EVALUATOR 3.0 model-checker of CADP

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:

• Memtime version 1.4 brings support for 64-bit architectures and a small patch for Solaris. It was prepared by Hubert Garavel, Frédéric Lang, and Wendelin Serwe. Precompiled executables of Memtime are provided for eight machine architectures.

Related sites:

• Original versions of Memtime (versions 1.0 to 1.3) by Johan Bengtsson at Uppsala University. No longer maintained since 2002. We used version 1.3 as a starting point.
• A parallel branch of Memtime developed at the University of Twente. A bunch of changes that we have neither reviewed nor tested.

---

Version 1.29 last updated on 2021/08/26 18:00:45

---

Back to the CADP Home Page