Selected publications about the CADP software
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:

Table of contents


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

See also the related manual pages at:
          http://cadp.inria.fr/man/installator.html
          http://cadp.inria.fr/man/svl.html
          http://cadp.inria.fr/man/tst.html
          http://cadp.inria.fr/man/xeuca.html


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
          http://cadp.inria.fr/man/lpp.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.

See also the related manual pages at:
          http://cadp.inria.fr/man/caesar.html
          http://cadp.inria.fr/man/caesar.bdd.html
          http://cadp.inria.fr/man/caesar.indent.html
          http://cadp.inria.fr/man/lotos.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 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.

See also the manual pages of the OPEN/CAESAR-compliant compilers at:
          http://cadp.inria.fr/man/bcg_open.html
          http://cadp.inria.fr/man/exp.open.html
          http://cadp.inria.fr/man/fsp.open.html
          http://cadp.inria.fr/man/lnt.open.html
          http://cadp.inria.fr/man/lotos.open.html
          http://cadp.inria.fr/man/seq.open.html

See also the manual pages of the OPEN/CAESAR application tools at:
          http://cadp.inria.fr/man/bisimulator.html
          http://cadp.inria.fr/man/cunctator.html
          http://cadp.inria.fr/man/declarator.html
          http://cadp.inria.fr/man/determinator.html
          http://cadp.inria.fr/man/distributor.html
          http://cadp.inria.fr/man/evaluator.html
          http://cadp.inria.fr/man/executor.html
          http://cadp.inria.fr/man/exhibitor.html
          http://cadp.inria.fr/man/generator.html
          http://cadp.inria.fr/man/ocis.html
          http://cadp.inria.fr/man/predictor.html
          http://cadp.inria.fr/man/projector.html
          http://cadp.inria.fr/man/reductor.html
          http://cadp.inria.fr/man/simulator.html
          http://cadp.inria.fr/man/terminator.html
          http://cadp.inria.fr/man/tgv.html
          http://cadp.inria.fr/man/xsimulator.html

See also the manual pages of the OPEN/CAESAR libraries at:
          http://cadp.inria.fr/man/caesar_area_1.html
          http://cadp.inria.fr/man/caesar_bitmap.html
          http://cadp.inria.fr/man/caesar_diagnostic_1.html
          http://cadp.inria.fr/man/caesar_edge.html
          http://cadp.inria.fr/man/caesar_graph.html
          http://cadp.inria.fr/man/caesar_hash.html
          http://cadp.inria.fr/man/caesar_hide_1.html
          http://cadp.inria.fr/man/caesar_mask_1.html
          http://cadp.inria.fr/man/caesar_rename_1.html
          http://cadp.inria.fr/man/caesar_solve_1.html
          http://cadp.inria.fr/man/caesar_stack_1.html
          http://cadp.inria.fr/man/caesar_standard.html
          http://cadp.inria.fr/man/caesar_table_1.html
          http://cadp.inria.fr/man/caesar_version.html


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

See also the manual pages of the BCG tools at:
          http://cadp.inria.fr/man/bcg_draw.html
          http://cadp.inria.fr/man/bcg_edit.html
          http://cadp.inria.fr/man/bcg_graph.html
          http://cadp.inria.fr/man/bcg_info.html
          http://cadp.inria.fr/man/bcg_io.html
          http://cadp.inria.fr/man/bcg_labels.html
          http://cadp.inria.fr/man/bcg_lib.html
          http://cadp.inria.fr/man/bcg_merge.html
          http://cadp.inria.fr/man/bcg_min.html
          http://cadp.inria.fr/man/bcg_open.html
          http://cadp.inria.fr/man/bcg_steady.html
          http://cadp.inria.fr/man/bcg_transient.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.

See also the related manual pages at:
          http://cadp.inria.fr/man/bisimulator.html
          http://cadp.inria.fr/man/reductor.html
          http://cadp.inria.fr/man/bcg_min.html


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.

See also the related manual pages at:
          http://cadp.inria.fr/man/exp.open.html
          http://cadp.inria.fr/man/projector.html
          http://cadp.inria.fr/man/svl.html
          http://cadp.inria.fr/man/reductor.html
          http://cadp.inria.fr/man/bcg_cmp.html
          http://cadp.inria.fr/man/bcg_min.html


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.

See also the related manual pages at:
          http://cadp.inria.fr/man/distributor.html
          http://cadp.inria.fr/man/bcg_merge.html
          http://cadp.inria.fr/man/gcf.html
          http://cadp.inria.fr/man/pbg.html
          http://cadp.inria.fr/man/pbg_cp.html
          http://cadp.inria.fr/man/pbg_info.html
          http://cadp.inria.fr/man/pbg_mv.html
          http://cadp.inria.fr/man/pbg_rm.html


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.

See also the related manual pages at:
          http://cadp.inria.fr/man/bcg_min.html
          http://cadp.inria.fr/man/bcg_steady.html
          http://cadp.inria.fr/man/bcg_transient.html
          http://cadp.inria.fr/man/cunctator.html
          http://cadp.inria.fr/man/determinator.html
          http://cadp.inria.fr/man/evaluator5.html


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.

See also the related manual pages at:
          http://cadp.inria.fr/man/caesar.bdd.html
          http://cadp.inria.fr/man/nupn.html
          http://cadp.inria.fr/man/nupn_info.html


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.140 - Date 2024/03/05 12:24:49
Back to the CADP Home Page