Selected publications about the CADP software


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

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

These selected papers are part of the comprehensive list of CADP-related publications.

Additional information can be obtained from:

the CADP manual pages

the VASY team publication page (1996-2011)

the CONVECS team publication page (2012-now)

Overview papers about CADP
Papers about compilers for the LNT language
Papers about compilers for the LOTOS language
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, 4, and 5
Papers about model checking using XTL
Papers about compositional verification
Papers about distributed verification
Papers about test generation
Papers about performance evaluation
Papers about concurrency models
Papers about translations for other languages
Papers about case studies and applications

Overview papers about CADP

CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
April 2013, 21 pages.

Additional material is available from: http://cadp.inria.fr/tutorial

Papers about compilers for the LNT language

(documentation about the LNT language itself is available here).

Papers about sequential code generation

Reference Manual of the LNT to LOTOS Translator
David Champelovier, Xavier Clerc, Hubert Garavel, Yves Guerte, Frédéric Lang, Wendelin Serwe, and Gideon Smeding
(regularly updated since 2005, around 150 pages).

See also the related manual pages at:
http://cadp.inria.fr/man/lnt.open.html
http://cadp.inria.fr/man/lnt2lotos.html

Papers about distributed code generation

Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes Interacting by Multiway Rendezvous
Hugues Evrard and Frédéric Lang
April 2017, 66 pages.

Papers about compilers for the LOTOS language

(documentation about the LOTOS language itself is available here).

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 related manual pages at:
http://cadp.inria.fr/man/caesar.adt.html
http://cadp.inria.fr/man/lotos.html

Papers about the CAESAR compiler for LOTOS processes

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

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
February 2006, 24 pages.

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 since 1992), about 200 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.

CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems
Radu Mateescu
July 2006, 39 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://cadp.inria.fr/man/bcg.html
http://cadp.inria.fr/man/bcg_read.html
http://cadp.inria.fr/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.

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

Papers about model checking using EVALUATOR 3, 4, and 5

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.

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

Property-Dependent Reductions for the Modal Mu-Calculus
Radu Mateescu and Anton Wijs
July 2011, 30 pages.

On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
Radu Mateescu and José Ignacio Requeno
August 2018, 24 pages.

See also the related manual pages at:
http://cadp.inria.fr/man/evaluator.html
http://cadp.inria.fr/man/caesar_solve_1.html

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.

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

Papers about compositional verification

Compositional Verification of Asynchronous Concurrent Systems using CADP
Hubert Garavel, Radu Mateescu, and Frédéric Lang
April 2015, 68 pages.

Compositional Verification in Action
Hubert Garavel, Frédéric Lang, and Laurent Mounier
September 2018, 27 pages.

The above publication provides a wide overview of compositional verification techniques using CADP; the publications below address more specialized topics.

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.

Smart Reduction
Pepijn Crouzen and Frédéric Lang
March 2011, 15 pages.

Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
April 2020, 20 pages.

Compositional Verification of Concurrent Systems by Combining Bisimulations
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
February 2021, 43 pages.

Compositional Verification of Priority Systems Using Sharp Bisimulation
Luca Di Stefano and Frédéric Lang
May 2023, 45 pages.

Papers about distributed verification

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

Distributed Local Resolution of Boolean Equation Systems
Christophe Joubert and Radu Mateescu
February 2005, 8 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.

Large-scale Distributed Verification using CADP: Beyond Clusters to Grids
Hubert Garavel, Radu Mateescu, and Wendelin Serwe
September 2012, 18 pages.

Papers about test generation

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.

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.

TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
Lina Marsso, Radu Mateescu, and Wendelin Serwe
April 2018, 17 pages.

See also the TGV manual page at:
http://cadp.inria.fr/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.

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

Ten Years of Performance Evaluation for Concurrent Systems Using CADP
Nicolas Coste, Hubert Garavel, Holger Hermanns, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
October 2010, 15 pages.

Papers about concurrency models

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

Nested-Unit Petri Nets
Hubert Garavel
April 2019, 51 pages.

Papers about translations for other languages

Papers about BPMN

Checking Business Process Evolution
Pascal Poizat, Gwen Salaun, and Ajay Krishna
October 2016, 18 pages.

Papers about CHP

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.

Papers about FSP

Translating FSP into LOTOS and Networks of Automata
Frédéric Lang, Gwen Salaün, Rémi Hérilier, Jeff Kramer, and Jeff Magee
November 2010, 34 pages.

Papers about GALS

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

Formal modelling and verification of GALS systems using GRL and CADP
Fatma Jebali, Frédéric Lang, and Radu Mateescu
May 2016, 38 pages.

Papers about Pi-Calculus

Translating Pi-Calculus into LOTOS NT
Radu Mateescu and Gwen Salaün
October 2010, 16 pages.

Papers about SystemC/TLM

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

A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS
Olivier Ponsini and Wendelin Serwe
May 2008, 16 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.

Papers about case studies and applications

Case-study papers are available from: http://cadp.inria.fr/case-studies

Version 2.141 - Date 2024/12/06 16:21:38

Back to the CADP Home Page

Table of contents