What is CADP?
Home Page Tools Overview Current Status
Installation
How to obtain CADP? Usage Statistics Issues & Patches
Documentation
Tutorials Publications Manual Pages Demo Examples FAQ
CADP Newsletters
Nr. 1 - Dec. 1996 Nr. 2 - Jun. 1997 Nr. 3 - Sep. 1997 Nr. 4 - Jan. 1999 Nr. 5 - Jul. 2001 Nr. 6 - Apr. 2007
CADP Community
Forum Education & Training Case Studies Research Tools
CADP Resources
VLTS Benchmarks Other Resources
About CADP
Contributors

1. The VLTS 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 is a joint project of CWI/SEN2 and INRIA/VASY.

---

2. 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).

---

3. Connecting the muCRL tools to the BCG format

A patch is available here that allows support of the BCG format in the muCRL toolset (versions 2.9.4 and 2.10.1). Once installed, you can use the instantiator tool of muCRL to generate compact .bcg files instead of huge .aut files.

This patch was developed by Frédéric Perret and Hubert Garavel (INRIA/VASY), and benefited from useful suggestions from Dr. Thomas Arts (Ericsson, Sweden).

---

Version 1.11 last updated on 11/11/24 14:42:40

---

Back to the VASY Home Page