Publications about the CADP software


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

This Page gives a list of scientific publications related to the CADP software.

Additional information can be obtained from:

the CADP Web Page

the VASY Publication Page

the CADP release, which provides more information than available on-line, such as installation guides, Application Programming Interfaces (including the OPEN/CAESAR Reference Manual), etc.

Overview papers about CADP
Papers about the CAESAR compiler for LOTOS processes
Papers about the CAESAR.ADT compiler for LOTOS data types
Papers about implicit state space manipulation using OPEN/CAESAR
Papers about explicit state space manipulation using BCG
Papers about equivalence checking using BISIMULATOR and REDUCTOR
Papers about model checking using EVALUATOR 3.* and 4.*
Papers about model checking using XTL
Papers about compositional verification using SVL
Papers about distributed verification
Papers about test generation using TGV
Papers about performance evaluation
Papers about case-studies and applications
Papers about LOTOS
Papers about other languages: E-LOTOS, LOTOS NT, NTIF, etc.
Old papers about CADP and EUCALYPTUS (outdated)
Old papers about equivalence checking using ALDEBARAN (outdated)
Old papers about model checking using EVALUATOR 2.0 (outdated)

Overview papers about CADP

An Overview of CADP 2001
Hubert Garavel, Frédéric Lang, and Radu Mateescu
December 2001, 15 pages.

CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
July 2007, 5 pages.

Additional material is available from: http://www.inrialpes.fr/vasy/cadp/tutorial

Papers about the CAESAR compiler for LOTOS processes

Compilation et Vérification de Programmes LOTOS
Hubert Garavel
November 1989, 265 pages, in French.

CAESAR Reference Manual
Hubert Garavel
November 1990, 32 pages.

Compilation and Verification of LOTOS Specifications
Hubert Garavel and Joseph Sifakis
June 1990, 18 pages.

State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe
July 2004, 17 pages.

State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe
February 2006, 24 pages.

Papers about the CAESAR.ADT compiler for LOTOS data types

Compilation of LOTOS Abstract Data Types
Hubert Garavel
December 1989, 20 pages.

CAESAR.ADT : Un Compilateur pour les Types Algébriques du Langage LOTOS
Hubert Garavel and Philippe Turlier
1993, 15 pages, in French.

See also the CAESAR.ADT manual page at:
http://www.inrialpes.fr/vasy/cadp/man/caesar.adt.html

Papers about implicit state space manipulation using OPEN/CAESAR

OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing
Hubert Garavel
March 1998, 18 pages.

The OPEN/CAESAR Reference Manual
Hubert Garavel
May 1992 (regularly updated), about 170 pages.

SEQ.OPEN: A Tool for Efficient Trace-Based Verification
Hubert Garavel and Radu Mateescu
April 2004, 6 pages.

Efficient Diagnostic Generation for Boolean Equation Systems
Radu Mateescu
January 2000, 23 pages.

A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
Radu Mateescu
April 2003, 21 pages.

On-the-Fly Verification using CADP
Radu Mateescu
June 2003, 5 pages.

CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems
Radu Mateescu
July 2006, 39 pages.

Behavioral Adaptation of Component Compositions based on Process Algebra Encodings
Radu Mateescu, Pascal Poizat, and Gwen Salaün
November 2007, 25 pages.

Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques
Radu Mateescu, Pascal Poizat, and Gwen Salaün
December 2008, 16 pages.

Hierarchical Adaptive State Space Caching based on Level Sampling
Radu Mateescu and Anton Wijs
March 2009, 15 pages.

Efficient On-the-Fly Computation of Weak Tau-Confluence
Radu Mateescu and Anton Wijs
July 2009, 42 pages.

Papers about explicit state space manipulation using BCG

The BCG Postscript Format
Louis-Pascal Tock
October 1995, 12 pages.

See also the manual pages of the BCG programming interfaces at:
http://www.inrialpes.fr/vasy/cadp/man/bcg.html
http://www.inrialpes.fr/vasy/cadp/man/bcg_read.html
http://www.inrialpes.fr/vasy/cadp/man/bcg_write.html

Papers about equivalence checking using BISIMULATOR and REDUCTOR

BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
Damien Bergamini, Nicolas Descoubes, Christophe Joubert, and Radu Mateescu
April 2005, 5 pages.

Calculating Tau-Confluence Compositionally
Gordon Pace, Frédéric Lang, and Radu Mateescu
September 2003, 23 pages.

On-the-Fly State Space Reductions for Weak Equivalences
Radu Mateescu
September 2005, 10 pages.

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems
Radu Mateescu and Emilie Oudot
June 2008, 2 pages.

Improved On-the-Fly Equivalence Checking using Boolean Equation Systems
Radu Mateescu and Emilie Oudot
August 2008, 31 pages.

Papers about model checking using EVALUATOR 3.* and 4.*

Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus
Radu Mateescu
September 1998, 8 pages.

Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Radu Mateescu
April 2002, 36 pages.

Logiques temporelles bas�es sur actions pour la v�rification des syst�mes asynchrones
Radu Mateescu
December 2003, 39 pages.

Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
Radu Mateescu and Mihaela Sighireanu
March 2003, 32 pages.

Computation Tree Regular Logic for Genetic Regulatory Networks
Radu Mateescu, Pedro Tiago Monteiro, Estelle Dumas, and Hidde de Jong
October 2008, 53 pages.

A Model Checking Language for Concurrent Value-Passing Systems
Radu Mateescu and Damien Thivolle
May 2008, 16 pages.

Papers about model checking using XTL

XTL: A Meta-Language and Tool for Temporal Logic Model-Checking
Radu Mateescu and Hubert Garavel
July 1998, 10 pages.

Vérification des propriétés temporelles des programmes parallèles
Radu Mateescu
April 1998, 274 pages.

See also the XTL manual page at:
http://www.inrialpes.fr/vasy/cadp/man/xtl.html

Papers about compositional verification using SVL

Compositional State Space Generation from Lotos Programs
Jean-Pierre Krimm and Laurent Mounier
April 1997, 20 pages.

SVL: a Scripting Language for Compositional Verification
Hubert Garavel and Frédéric Lang
July 2001, 36 pages.

Compositional Verification using SVL Scripts
Frédéric Lang
April 2002, 5 pages.

EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods
Frédéric Lang
September 2005, 21 pages.

Refined Interfaces for Compositional Verification
Fr�d�ric Lang
September 2006, 22 pages.

Partial Order Reductions using Compositional Confluence Detection
Frederic Lang and Radu Mateescu
November 2009, 16 pages.

Papers about distributed verification

Parallel State Space Construction for Model-Checking
Hubert Garavel, Radu Mateescu, and Irina Smarandache
March 2001, 20 pages.

Distributed On-the-Fly Equivalence Checking
Christophe Joubert and Radu Mateescu
September 2004, 15 pages.

Distributed Local Resolution of Boolean Equation Systems
Christophe Joubert and Radu Mateescu
February 2005, 8 pages.

V�rification distribu�e � la vol�e de grands espaces d��tats
Christophe Joubert
December 2005, 172 pages.

DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation
Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier
March 2006, 5 pages.

Distributed On-the-Fly Model Checking and Test Case Generation
Christophe Joubert and Radu Mateescu
April 2006, 24 pages.

Papers about test generation using TGV

Using On-the-Fly Verification Techniques for the Generation of Test Suites
Jean-Claude Fernandez, Claude Jard, Thierry Jéron, Laurence Nedelka, and César Viho
August 1996, 14 pages.

An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology
Jean-Claude Fernandez, Claude Jard, Thierry Jéron, Laurence Nedelka, and César Viho
July 1997, 23 pages.

An Industrial Experiment in Automatic Generation of Executable Test Suites for a Cache Coherency Protocol
Hakim Kahlouche, César Viho, and Massimo Zendri
September 1998, 16 pages.

Hardware Testing using a Communication Protocol Conformance Testing Tool
Hakim Kahlouche, César Viho, and Massimo Zendri
March 1999, 15 pages.

TGV: Theory, Principles and Algorithms - A Tool for the Automatic Synthesis of Conformance Test Cases for Non-Deterministic Reactive Systems
Claude Jard and Thierry Jéron
August 2005, 19 pages.

See also the TGV manual page at:
http://www.inrialpes.fr/vasy/cadp/man/tgv.html

Papers about performance evaluation

On Combining Functional Verification and Performance Evaluation using CADP
Hubert Garavel and Holger Hermanns
July 2002, 24 pages.

A Set of Performance and Dependability Analysis Components for CADP
Holger Hermanns and Christophe Joubert
April 2003, 6 pages.

Modeling Multiprocessor Cache Protocol Impact on MPI Performance
Ghassan Chehaibar, Meriem Zidouni, and Radu Mateescu
May 2009, 6 pages.

Towards Performance Prediction of Compositional Models in Industrial GALS Designs
Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, and Wendelin Serwe
July 2009, 15 pages.

Papers about case-studies and applications

Utilisation de CAESAR et ALDEBARAN
Hubert Garavel
November 1989, 24 pages, in French.

An Example of LOTOS Specification: the Matrix Switch Problem
Hubert Garavel and Carlos Rodríguez
June 1990, 12 pages.

An Experiment with the LOTOS Formal Description Technique on the Flight Warning Computer of Airbus 330/340 Aircrafts
Hubert Garavel and René-Pierre Hautbois
November 1993, 20 pages.

A LOTOS Specification of a "Transit-Node"
Laurent Mounier
March 1994, 39 pages.

Formal Specification of a Framework for Groupware Development
Alain Kerbrat and Slim Ben Atallah
October 1995, 8 pages.

Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS
Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, and Ferruccio Zulian
October 1996, 20 pages.

Specification and Verification of various Distributed Leader Election Algorithms for Unidirectional Ring Networks
Hubert Garavel and Laurent Mounier
July 1997, 35 pages.

Formal Description and Analysis of a Bounded Retransmission Protocol
Radu Mateescu
June 1996, 31 pages.

Specification and Verification of the CO4 Distributed Knowledge System Using LOTOS
Charles Pecheur
November 1997, 97 pages.

Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS
Mihaela Sighireanu and Radu Mateescu
June 1997, 37 pages.

Advanced Modelling and Verification Techniques Applied to a Cluster File System
Charles Pecheur
May 1998, 55 pages.

Advanced Modelling and Verification Techniques Applied to a Cluster File System
Charles Pecheur
October 1999, 8 pages.

Requirement Capture, Formal Description and Verification of an Invoicing System
Mihaela Sighireanu and Ken Turner
December 1998, 32 pages.

System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation
Hubert Garavel, César Viho, and Massimo Zendri
November 2000, 36 pages.

Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications
Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, and Noel de Palma
July 2001, 32 pages.

Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components
Frédéric Tronel, Frédéric Lang, and Hubert Garavel
November 2003, 28 pages.

Model Checking Genetic Regulatory Networks using GNA and CADP
Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, and Radu Mateescu
April 2004, 6 pages.

Encoding Abstract Descriptions into Executable Web Services: Towards a Formal Development
Antonella Chirichiello and Gwen Sala�n
September 2005, 25 pages.

Modélisation et analyse de systèmes asynchrones avec CADP
Radu Mateescu
July 2006, 31 pages.

Formal Verification of CHP Specifications with CADP - Illustration on an Asynchronous Network-on-Chip
Gwen Salaün, Wendelin Serwe, Yvain Thonnart, and Pascal Vivet
March 2007, 10 pages.

Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures
Nicolas Coste, Hubert Garavel, Holger Hermanns, Richard Hersemeule, Yvain Thonnart, and Meriem Zidouni
March 2008, 2 pages.

Specification and Analysis of Asynchronous Systems using CADP
Radu Mateescu
March 2008, 28 pages.

Formal Modeling and Discrete-Time Analysis of BPEL Web Services
Radu Mateescu and Sylvain Rampacek
June 2008, 15 pages.

Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
Hubert Garavel and Damien Thivolle
June 2009, 20 pages.

More case-study papers are available from: http://www.inrialpes.fr/vasy/cadp/case-studies

Papers about LOTOS

Presentation du langage LOTOS
Hubert Garavel
November 1989, 38 pages, in French.

Introduction au Langage LOTOS
Hubert Garavel
1990, 14 pages, in French.

Defect Report Concerning ISO Standard 8807 and Proposal for a Correct Flattening of LOTOS Parameterized Types
Hubert Garavel and Mihaela Sighireanu
July 1995, 9 pages.

More LOTOS-related papers are available from: http://www.inrialpes.fr/vasy/cadp/tutorial

Papers about other languages: E-LOTOS, LOTOS NT, NTIF, etc.

On the Introduction of Gate Typing in E-LOTOS
Hubert Garavel
June 1995, 16 pages.

On the Introduction of Exceptions in E-LOTOS
Hubert Garavel and Mihaela Sighireanu
October 1996, 16 pages.

Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS
Hubert Garavel and Mihaela Sighireanu
May 1998, 28 pages.

Contribution à la Définition et à l'Implémentation du Langage E-LOTOS
Mihaela Sighireanu
January 1999, 300 pages.

A Graphical Parallel Composition Operator for Process Algebras
Hubert Garavel and Mihaela Sighireanu
October 1999, 18 pages.

Compiler Construction using LOTOS NT
Hubert Garavel, Frédéric Lang, and Radu Mateescu
April 2002, 5 pages.

NTIF: A General Symbolic Model for Communicating Sequential Processes with Data
Hubert Garavel and Frédéric Lang
December 2002, 30 pages.

D�fense et illustration des alg�bres de processus
Hubert Garavel
September 2003, 25 pages.

Translating Hardware Process Algebras into Standard Process Algebras - Illustration with CHP and LOTOS
Gwen Salaün and Wendelin Serwe
September 2005, 25 pages.

Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular
Hubert Garavel
December 2007, 16 pages.

A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS
Olivier Ponsini and Wendelin Serwe
May 2008, 16 pages.

A Comparison of Two SystemC/TLM Semantics for Formal Verification
Claude Helmstetter and Olivier Ponsini
June 2008, 10 pages.

On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP
Hubert Garavel, Gwen Salaün, and Wendelin Serwe
January 2009, 35 pages.

Verification of an Industrial SystemC/TLM Model using LOTOS and CADP
Hubert Garavel, Claude Helmstetter, Olivier Ponsini, and Wendelin Serwe
July 2009, 10 pages.

TLM.OPEN: a SystemC/TLM Front-End for the CADP Verification Toolbox
Claude Helmstetter
October 2009, 9 pages.

Other technical papers about E-LOTOS are available from: http://www.inrialpes.fr/vasy/elotos

Old papers about CADP and EUCALYPTUS (outdated)

Une Boîte à Outils pour la Vérification de Programmes LOTOS
Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, and Joseph Sifakis
September 1991, 22 pages, in French.

A Toolbox for the Verification of LOTOS Programs
Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, and Joseph Sifakis
May 1992, 14 pages.

CADP: A Protocol Validation and Verification Toolbox
Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Radu Mateescu, Laurent Mounier, and Mihaela Sighireanu
August 1996, 4 pages.

An Overview of the Eucalyptus Toolbox
Hubert Garavel
June 1996, 13 pages.

CADP'97 - Status, Applications, and Perspectives
Hubert Garavel, Mark Jorgensen, Radu Mateescu, Charles Pecheur, Mihaela Sighireanu, and Bruno Vivien
June 1997, 6 pages.

Old papers about equivalence checking using ALDEBARAN (outdated)

Aldebaran: A Tool for Verification of Communicating Processes
Jean-Claude Fernandez
September 1989, 28 pages.

Aldebaran User's Manual
Jean-Claude Fernandez
January 1989, 7 pages.

An Implementation of an Efficient Algorithm for Bisimulation Equivalence
Jean-Claude Fernandez
May 1990, 17 pages.

Verifying Bisimulations ``On the Fly''
Jean-Claude Fernandez and Laurent Mounier
November 1990, 16 pages.

``On the Fly'' Verification of Behavioural Equivalences and Preorders
Jean-Claude Fernandez and Laurent Mounier
July 1991, 13 pages.

A Tool Set for Deciding Behavioral Equivalences
Jean-Claude Fernandez and Laurent Mounier
August 1991, 20 pages.

Méthodes de Vérification de Spécifications Comportementales : Étude et Mise en Oeuvre
Laurent Mounier
January 1992, 203 pages, in French.

Symbolic Equivalence Checking
Jean-Claude Fernandez, Alain Kerbrat, and Laurent Mounier
June 1993, 12 pages.

Reachable State Space Analysis of LOTOS programs
Alain Kerbrat
October 1994, 16 pages.

See also the ALDEBARAN 7.0 manual page at:
http://www.inrialpes.fr/vasy/cadp/man/aldebaran.html

Old papers about model checking using EVALUATOR 2.0 (outdated)

A Local Checking Algorithm for Boolean Equation Systems
Jean-Claude Fernandez and Laurent Mounier
March 1995, 15 pages.

Version 2.34 - Date 10/02/02 19:01:46

Back to the VASY Home Page

Table of contents