All publications about the CADP software
This Page gives a comprehensive list of scientific publications related to the CADP software, in reverse chronological order.

There is also a shorter list of selected publications ordered by subject.



| 2016 | 2015 | 2014 | 2013 | 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 | 1995 | 1994 | 1993 | 1992 | 1991 | 1990 | 1989 | 1988 |

The following tags are used to label certain papers:

  paper about the LOTOS language (now subsumed by LNT)
  paper about software that is no longer part of CADP
  paper subsumed by a more recent paper or manual page
  paper describing a concrete application done using CADP
  (this tag usually links to the corresponding case-study page)
  paper reporting about a software tool connected to CADP
  (this tag usually links to the corresponding tool page)



- 2016 -

Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications
Rim Abid, Gwen Salaün, and Noël de Palma

February 2016, 35 pages.

An Improved Fault-Tolerant Routing Algorithm for a Network-on-Chip Derived with Formal Analysis
Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers

March 2016, 35 pages.

Verification of EB3 specifications using CADP
Dimitris Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu

March 2016, 34 pages.

DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
Hugues Evrard

April 2016, 6 pages.

On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
Radu Mateescu and José Ignacio Requeno

April 2016, 18 pages.

VerChor: A Framework for the Design and Verification of Choreographies
Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Lina Ye

June 2016, 14 pages.

Reliable Self-deployment of Distributed Cloud Applications
Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, and Noël de Palma

June 2016, 18 pages.

Formal Modelling and Verification of GALS Systems using GRL and CADP
Fatma Jebali, Frédéric Lang, and Radu Mateescu

June 2016, 38 pages.

MCC'2015 - The Fifth Model Checking Contest
Fabrice Kordon, Hubert Garavel, Lom Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, César Rodríguez, and Francis Hulin-Hubard

September 2016, 11 pages.

Checking Business Process Evolution
Pascal Poizat, Gwen Salaun, and Ajay Krishna

October 2016, 18 pages.


- 2015 -

Debugging Process Algebra Specifications
Gwen Salaün and Lina Ye

January 2015, 18 pages.

Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes
Hugues Evrard and Frédéric Lang

March 2015, 8 pages.

Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
Abderahman Kriouile and Wendelin Serwe

April 2015, 15 pages.

Compositional Verification of Asynchronous Concurrent Systems using CADP
Hubert Garavel, Frédéric Lang, and Radu Mateescu

April 2015, 68 pages.

Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets
Hubert Garavel

June 2015, 21 pages.

Asynchronous Coordination of Stateful Autonomic Managers in the Cloud
Rim Abid, Gwen Salaün, Noël de Palma, and Soguy Mak-Kare Gueye

October 2015, 18 pages.

Revisiting Sequential Composition in Process Calculi
Hubert Garavel

November 2015, 40 pages.

Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
Wendelin Serwe

November 2015, 87 pages.


- 2014 -

Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP
Etienne Lantreibecq and Wendelin Serwe

February 2014, 30 pages.

Reliable Self-Deployment of Cloud Applications
Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, and Noël de Palma

March 2014, 8 pages.

GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems (Syntax and Formal Semantics)
Fatma Jebali, Frédéric Lang, and Radu Mateescu

March 2014, 82 pages.

A Model-based Certification Framework for the EnergyBus Standard
Alexander Graf-Brill, Holger Hermanns, and Hubert Garavel

June 2014, 17 pages.

Quantifying the Parallelism in BPMN Processes using Model Checking
Radu Mateescu, Gwen Salaün, and Lina Ye

July 2014, 10 pages.

Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip
Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers

September 2014, 15 pages.

GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems
Fatma Jebali, Frédéric Lang, and Radu Mateescu

November 2014, 16 pages.

Property-Dependent Reductions Adequate with Divergence-Sensitive Branching Bisimilarity
Radu Mateescu and Anton Wijs

December 2014, 46 pages.


- 2013 -

Génération et manipulation d'espaces d'états distribués avec CADP: expériences sur Grid'5000
Hubert Garavel, Radu Mateescu, and Wendelin Serwe

January 2013, 18 pages, in French.

Verification of a Self-configuration Protocol for Distributed Applications in the Cloud
Gwen Salaün, Xavier Etchevers, Noël de Palma, Fabienne Boyer, and Thierry Coupaye

January 2013, 20 pages.

VerChor: A Framework for Verifying Choreographies
Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Alexandre Dumont

March 2013, 4 pages.

Composition and abstraction of logical regulatory modules: application to multicellular systems
Nuno Mendes, Frédéric Lang, Yves-Stan Le Cornec, Radu Mateescu, Grégory Batt, and Claudine Chaouiya

March 2013, 9 pages.

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.

An Experience Report on the Verification of Autonomic Protocols in the Cloud
Gwen Salaün, Fabienne Boyer, Thierry Coupaye, Noël de Palma, Xavier Etchevers, and Olivier Gruber

June 2013, 23 pages.

Formal Verification of Distributed Branching Multiway Synchronization Protocols
Hugues Evrard and Frédéric Lang

June 2013, 20 pages.

Translating EB3 to LNT for verification with CADP
Dimitrios Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu

June 2013, 16 pages.

Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols
Radu Mateescu and Wendelin Serwe

July 2013, 18 pages.

Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip
Abderahman Kriouile and Wendelin Serwe

September 2013, 15 pages.

Compatibility Checking for Asynchronously Communicating Software
Meriem Ouederni, Gwen Salaün, and Tevfik Bultan

October 2013, 18 pages.

Verification of a Dynamic Management Protocol for Cloud Applications
Rim Abid, Gwen Salaün, Francesco Bongiovanni, and Noël de Palma

October 2013, 15 pages.

Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
Frédéric Lang and Radu Mateescu

October 2013, 28 pages.


- 2012 -

Checking the Realizability of BPMN 2.0 Choreographies
Pascal Poizat and Gwen Salaün

March 2012, 8 pages.

Verification of a Self-configuration Protocol for Distributed Applications in the Cloud
Gwen Salaün, Xavier Etchevers, Noël de Palma, Fabienne Boyer, and Thierry Coupaye

March 2012, 6 pages.

Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
Frédéric Lang and Radu Mateescu

March 2012, 28 pages.

Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques
Radu Mateescu, Pascal Poizat, and Gwen Salaün

July 2012, 25 pages.

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

September 2012, 18 pages.

Realizability of Choreographies using Process Algebra Encodings
Gwen Salaün, Tevfik Bultan, and Nima Roohi

September 2012, 14 pages.

Sequential and Distributed On-the-Fly Computation of Weak Tau-Confluence
Radu Mateescu and Anton Wijs

September 2012, 38 pages.

Counterexample Guided Synthesis of Monitors for Realizability Enforcement
Matthias Güdemann, Gwen Salaün, and Meriem Ouederni

October 2012, 16 pages.


- 2011 -

CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe

March 2011, 15 pages.

Smart Reduction
Pepijn Crouzen and Frédéric Lang

March 2011, 15 pages.

Langages modernes pour la vérification des systèmes asynchrones
Damien Thivolle

April 2011, in French.

Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
Fabienne Boyer, Olivier Gruber, and Gwen Salaün

June 2011, 15 pages.

Property-Dependent Reductions for the Modal Mu-Calculus
Radu Mateescu and Anton Wijs

July 2011, 30 pages.

CTRL: Extension of CTL with Regular Expressions and Fairness Operators to Verify Genetic Regulatory Networks
Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, and Hidde de Jong

July 2011, 65 pages.

Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP
Etienne Lantreibecq and Wendelin Serwe

August 2011, 16 pages.

Self-configuration of Legacy Distributed Applications in the Cloud
Xavier Etchevers, Thierry Coupaye, Fabienne Boyer, Noël de Palma, and Gwen Salaün

December 2011, 8 pages.


- 2010 -

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 130 pages).

Towards Performance Prediction of Compositional Models in GALS Designs
Nicolas Coste

June 2010, 223 pages.

A Study of Shared-Memory Mutual Exclusion Protocols using CADP
Radu Mateescu and Wendelin Serwe

September 2010, 18 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.

Translating Pi-Calculus into LOTOS NT
Radu Mateescu and Gwen Salaün

October 2010, 16 pages.

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.


- 2009 -

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.

Hierarchical Adaptive State Space Caching based on Level Sampling
Radu Mateescu and Anton Wijs

March 2009, 15 pages.

Modeling Multiprocessor Cache Protocol Impact on MPI Performance
Ghassan Chehaibar, Meriem Zidouni, and Radu Mateescu

May 2009, 6 pages.

Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
Hubert Garavel and Damien Thivolle

June 2009, 20 pages.

Efficient On-the-Fly Computation of Weak Tau-Confluence
Radu Mateescu and Anton Wijs

July 2009, 42 pages.

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

July 2009, 15 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.

Partial Order Reductions using Compositional Confluence Detection
Frédéric Lang and Radu Mateescu

November 2009, 16 pages.


- 2008 -

FIACRE: An Intermediate Language for Model Verification in the TopCased Environment
Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gaufillet, Frédéric Lang, and François Vernadat

January 2008, 8 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.

A Model Checking Language for Concurrent Value-Passing Systems
Radu Mateescu and Damien Thivolle

May 2008, 16 pages.

A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS
Olivier Ponsini and Wendelin Serwe

May 2008, 16 pages.

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems
Radu Mateescu and Emilie Oudot

June 2008, 2 pages.

A Comparison of Two SystemC/TLM Semantics for Formal Verification
Claude Helmstetter and Olivier Ponsini

June 2008, 10 pages.

Formal Modeling and Discrete-Time Analysis of BPEL Web Services
Radu Mateescu and Sylvain Rampacek

June 2008, 15 pages.

Improved On-the-Fly Equivalence Checking using Boolean Equation Systems
Radu Mateescu and Emilie Oudot

August 2008, 31 pages.

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

October 2008, 53 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.


- 2007 -

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.

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.

Translating FSP into LOTOS and Networks of Automata
Gwen Salaün, Jeff Kramer, Frédéric Lang, and Jeff Magee

July 2007, 21 pages.

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

November 2007, 25 pages.

Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular
Hubert Garavel

December 2007, 16 pages.


- 2006 -

State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe

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

Synchronizing Behavioural Mismatch in Software Composition
Carlos Canal, Pascal Poizat, and Gwen Salaün

June 2006, 15 pages.

CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems
Radu Mateescu

July 2006, 39 pages.

Modélisation et analyse de systèmes asynchrones avec CADP
Radu Mateescu

July 2006, 31 pages, in French.

Refined Interfaces for Compositional Verification
Frédéric Lang

September 2006, 22 pages.


- 2005 -

Distributed Local Resolution of Boolean Equation Systems
Christophe Joubert and Radu Mateescu

February 2005, 8 pages.

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

April 2005, 5 pages.

Analysis and Verification of Qualitative Models of Genetic Regulatory Networks: A Model-Checking Approach
Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider

July-August 2005, 6 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.

Encoding Abstract Descriptions into Executable Web Services: Towards a Formal Development
Antonella Chirichiello and Gwen Salaün

September 2005, 25 pages.

On-the-Fly State Space Reductions for Weak Equivalences
Radu Mateescu

September 2005, 10 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.

Translating Hardware Process Algebras into Standard Process Algebras - Illustration with CHP and LOTOS
Gwen Salaün and Wendelin Serwe

September 2005, 25 pages.

Vérification distribuée à la volée de grands espaces d´états
Christophe Joubert

December 2005, 172 pages, in French.

Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli
Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider

December 2005, 10 pages.


- 2004 -

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.

SEQ.OPEN: A Tool for Efficient Trace-Based Verification
Hubert Garavel and Radu Mateescu

April 2004, 6 pages.

State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe

July 2004, 17 pages.

Distributed On-the-Fly Equivalence Checking
Christophe Joubert and Radu Mateescu

September 2004, 15 pages.


- 2003 -

Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
Radu Mateescu and Mihaela Sighireanu

March 2003, 32 pages.

A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
Radu Mateescu

April 2003, 21 pages.

A Set of Performance and Dependability Analysis Components for CADP
Holger Hermanns and Christophe Joubert

April 2003, 6 pages.

On-the-Fly Verification using CADP
Radu Mateescu

June 2003, 5 pages.

Distributed Model Checking: From Abstract Algorithms to Concrete Implementations
Christophe Joubert

July 2003, 14 pages.

Calculating Tau-Confluence Compositionally
Gordon Pace, Frédéric Lang, and Radu Mateescu

September 2003, 23 pages.

Défense et illustration des algèbres de processus
Hubert Garavel

September 2003, 25 pages, in French.

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.

Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones
Radu Mateescu

December 2003, 39 pages, in French.


- 2002 -

Compositional Verification using SVL Scripts
Frédéric Lang

April 2002, 5 pages.

Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Radu Mateescu

April 2002, 36 pages.

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

On Combining Functional Verification and Performance Evaluation using CADP
Hubert Garavel and Holger Hermanns

July 2002, 24 pages.

NTIF: A General Symbolic Model for Communicating Sequential Processes with Data
Hubert Garavel and Frédéric Lang

December 2002, 30 pages.


- 2001 -

Parallel State Space Construction for Model-Checking
Hubert Garavel, Radu Mateescu, and Irina Smarandache

March 2001, 20 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.

SVL: a Scripting Language for Compositional Verification
Hubert Garavel and Frédéric Lang

July 2001, 36 pages.

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

December 2001, 15 pages.


- 2000 -

Efficient Diagnostic Generation for Boolean Equation Systems
Radu Mateescu

January 2000, 23 pages.

Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
Radu Mateescu and Mihaela Sighireanu

March 2000, 24 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.


- 1999 -

Contribution à la Définition et à l'Implémentation du Langage E-LOTOS
Mihaela Sighireanu

January 1999, 300 pages, in French.

Hardware Testing using a Communication Protocol Conformance Testing Tool
Hakim Kahlouche, César Viho, and Massimo Zendri

March 1999, 15 pages.

Advanced Modelling and Verification Techniques Applied to a Cluster File System
Charles Pecheur

October 1999, 8 pages.

A Graphical Parallel Composition Operator for Process Algebras
Hubert Garavel and Mihaela Sighireanu

October 1999, 18 pages.


- 1998 -

Model-Checking Validation of the LOTOS Descriptions of the Invoicing Case Study
Mihaela Sighireanu

March 1998, 16 pages.

OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing
Hubert Garavel

March 1998, 18 pages.

Vérification des propriétés temporelles des programmes parallèles
Radu Mateescu

April 1998, 274 pages, in French.

Advanced Modelling and Verification Techniques Applied to a Cluster File System
Charles Pecheur

May 1998, 55 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.

XTL: A Meta-Language and Tool for Temporal Logic Model-Checking
Radu Mateescu and Hubert Garavel

July 1998, 10 pages.

Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus
Radu Mateescu

September 1998, 8 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.

Requirement Capture, Formal Description and Verification of an Invoicing System
Mihaela Sighireanu and Ken Turner

December 1998, 32 pages.


- 1997 -

Compositional State Space Generation from Lotos Programs
Jean-Pierre Krimm and Laurent Mounier

April 1997, 20 pages.

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

June 1997, 6 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.

Specification and Verification of the CO4 Distributed Knowledge System Using LOTOS
Charles Pecheur

November 1997, 97 pages.


- 1996 -

An Overview of the Eucalyptus Toolbox
Hubert Garavel

June 1996, 13 pages.

Formal Description and Analysis of a Bounded Retransmission Protocol
Radu Mateescu

June 1996, 31 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

June 1996, 23 pages.

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.

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.

Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks
Hubert Garavel and Laurent Mounier

September 1996, 35 pages.

On the Introduction of Exceptions in E-LOTOS
Hubert Garavel and Mihaela Sighireanu

October 1996, 16 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.


- 1995 -

A Local Checking Algorithm for Boolean Equation Systems
Jean-Claude Fernandez and Laurent Mounier

March 1995, 15 pages.

On the Introduction of Gate Typing in E-LOTOS
Hubert Garavel

June 1995, 16 pages.

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.

The BCG Postscript Format
Louis-Pascal Tock

October 1995, 12 pages.

Formal Specification of a Framework for Groupware Development
Alain Kerbrat and Slim Ben Atallah

October 1995, 8 pages.


- 1994 -

A LOTOS Specification of a "Transit-Node"
Laurent Mounier

March 1994, 39 pages.

Reachable State Space Analysis of LOTOS programs
Alain Kerbrat

October 1994, 16 pages.


- 1993 -

CAESAR.ADT : Un Compilateur pour les Types Algébriques du Langage LOTOS
Hubert Garavel and Philippe Turlier

1993, 15 pages, in French.

Symbolic Equivalence Checking
Jean-Claude Fernandez, Alain Kerbrat, and Laurent Mounier

June 1993, 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.


- 1992 -

Méthodes de Vérification de Spécifications Comportementales : Étude et Mise en Oeuvre
Laurent Mounier

January 1992, 203 pages, in French.

The OPEN/CAESAR Reference Manual
Hubert Garavel

May 1992 (regularly updated since 1992), about 200 pages.

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.


- 1991 -

``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.

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.


- 1990 -

An Implementation of an Efficient Algorithm for Bisimulation Equivalence
Jean-Claude Fernandez

May 1990, 17 pages.

An Example of LOTOS Specification: the Matrix Switch Problem
Hubert Garavel and Carlos Rodriguez

June 1990, 12 pages.

Compilation and Verification of LOTOS Specifications
Hubert Garavel and Joseph Sifakis

June 1990, 18 pages.

CAESAR Reference Manual
Hubert Garavel

November 1990, 32 pages.

Verifying Bisimulations ``On the Fly''
Jean-Claude Fernandez and Laurent Mounier

November 1990, 16 pages.

Introduction au Langage LOTOS
Hubert Garavel

1990, 14 pages, in French.


- 1989 -

Aldebaran User's Manual
Jean-Claude Fernandez

January 1989, 7 pages.

Aldebaran: A Tool for Verification of Communicating Processes
Jean-Claude Fernandez

September 1989, 28 pages.

Compilation et Vérification de Programmes LOTOS
Hubert Garavel

November 1989, 265 pages, in French.

Presentation du langage LOTOS
Hubert Garavel

November 1989, 38 pages, in French.

Utilisation de CAESAR et ALDEBARAN
Hubert Garavel

November 1989, 24 pages, in French.

Compilation of LOTOS Abstract Data Types
Hubert Garavel

December 1989, 20 pages.


- 1988 -

ALDEBARAN : un Système de Vérification par Réduction de Processus Communicants
Jean-Claude Fernandez

May 1988, 196 pages, in French.


Version 1.39 - Date 2016/11/16 15:01:24
Back to the CADP Home Page