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 casestudy page) 

paper reporting about a software tool connected to CADP (this tag usually links to the corresponding tool page) 
Four Formal Models of IEEE 1394 Link Layer
Hubert Garavel and Bas Luttik
April 2024, 80 pages.
Testing Resource Isolation for SystemonChip Architectures
Philippe Ledent, Radu Mateescu, and Wendelin Serwe
April 2024, 40 pages.
Compositional Verification of Stigmergic Collective Systems
Luca Di Stefano and Frédéric Lang
January 2023, 22 pages.
Compositional Verification of Priority Systems Using Sharp Bisimulation
Luca Di Stefano and Frédéric Lang
May 2023, 45 pages.
A Toolchain to Compute Concurrent Places of Petri Nets
Nicolas Amat, Pierre Bouvier, and Hubert Garavel
November 2023, 28 pages.
Design and Deployment of Expressive and Correct Web of Things Applications
Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün
February 2022, 30 pages.
Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles
JeanBaptiste Horel, Christian Laugier, Lina Marsso, Radu Mateescu, Lucie Muller, Anshul Paigwar, Alessandro Renzaglia, and Wendelin Serwe
March 2022, 6 pages.
Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
Lina Marsso, Radu Mateescu, Lucie Muller, and Wendelin Serwe
April 2022, 58 pages.
Counting Bugs in Behavioural Models using Counterexample Analysis
Irman Faqrizal and Gwen Salaün
May 2022, 11 pages.
Probabilistic Model Checking of BPMN Processes at Runtime
Yliès Falcone, Gwen Salaün, and Ahang Zuo
June 2022, 18 pages.
Models and Analysis for Userdriven Reconfiguration of Rulebased IoT Applications
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün
June 2022, 39 pages.
Equivalence Checking 40 Years After: A Review of Bisimulation Tools
Hubert Garavel and Frédéric Lang
September 2022, 64 pages.
Probabilistic Analysis of Industrial IoT Applications
Yliès Falcone, Irman Faqrizal, and Gwen Salaün
November 2022, 8 pages.
Compositional Verification of Concurrent Systems by Combining Bisimulations
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
February 2021, 43 pages.
Quantifying the Similarity of Nonbisimilar Labelled Transition Systems
Gwen Salaün
February 2021, 25 pages.
Efficient Algorithms for Three Reachability Problems in Safe Petri Nets
Pierre Bouvier and Hubert Garavel
June 2021, 23 pages.
Debugging of Behavioural Models using Counterexample Analysis
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
June 2021, 14 pages.
Consistent Substitution of Object in Rulebased IoT Applications
Gwen Salaün
July 2021, 9 pages.
The VLSAT2 Benchmark Suite
Pierre Bouvier and Hubert Garavel
September 2021, 8 pages.
Verifying Temporal Properties of Stigmergic Collective Systems Using CADP
Luca Di Stefano and Frédéric Lang
October 2021, 16 pages.
Is CADP an Applicable Formal Method?
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
November 2021, 11 pages.
The VLSAT3 Benchmark Suite
Pierre Bouvier
December 2021, 20 pages.
Using Model Checking to Identify Timing Interferences on Multicore Processors
Viet Anh Nguyen, Eric Jenn, Wendelin Serwe, Frédéric Lang, and Radu Mateescu
January 2020, 10 pages.
Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin
April 2020, 40 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.
MOZART: Design and Deployment of Advanced IoT Applications
Ajay Krishna, Michel Le Pallec, Alejandro Martinez, Radu Mateescu, and Gwen Salaün
April 2020, 4 pages.
Automatic Decomposition of Petri Nets into Automata Networks  A Synthetic Account
Pierre Bouvier, Hubert Garavel, and Hernán Ponce de León
June 2020, 24 pages.
Combining SLiVER with CADP to Analyze Multiagent Systems
Luca Di Stefano, Frédéric Lang, and Wendelin Serwe
June 2020, 15 pages.
The 2020 Expert Survey on Formal Methods
Hubert Garavel, Maurice ter Beek, and Jaco van de Pol
August 2020, 67 pages.
Verification of a Failure Management Protocol for Stateful IoT Applications
Umar Ozeer, Gwen Salaün, Loïc Letondeur, FrançoisGaël Ottogalli, and JeanMarc Vincent
September 2020, 16 pages.
The VLSAT1 Benchmark Suite
Pierre Bouvier and Hubert Garavel
November 2020, 6 pages.
Clusters of Faulty States for Debugging Behavioural Models
Irman Faqrizal and Gwen Salaün
December 2020, 9 pages.
Automated Transition Coverage in Behavioural Conformance Testing
Lina Marsso, Radu Mateescu, and Wendelin Serwe
December 2020, 17 pages.
Proposal for Adding Useful Features to PetriNet Model Checkers
Hubert Garavel
December 2020, 6 pages.
Models and Verification for Composition and Reconfiguration of Web of Things Applications
Ajay Krishna
December 2020, 143 pages.
Checking Business Process Evolution
Ajay Krishna, Pascal Poizat, and Gwen Salaün
January 2019, 49 pages.
NestedUnit Petri Nets
Hubert Garavel
April 2019, 51 pages.
TOOLympics 2019: An Overview of Competitions in Formal Methods
Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, and Akihisa Yamada.
April 2019, 22 pages.
The Rewrite Engines Competitions: A RECtrospective
Francisco Durán and Hubert Garavel.
April 2019, 9 pages.
Visual Debugging of Behavioural Models
Gianluca Barbon, Vincent Leroy, Gwen Salaün, and Emmanuel Yah
May 2019, 4 pages.
IoT Composer: Composition and Deployment of IoT Applications
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, and Gwen Salaün
May 2019, 4 pages.
Rigorous Design and Deployment of IoT Applications
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, and Gwen Salaün
May 2019, 10 pages.
Reflections on Bernhard Steffen's Physics of Software Tools
Hubert Garavel and Radu Mateescu.
June 2019, 25 pages.
Quantifying the Similarity of Nonbisimilar Labelled Transition Systems
Gwen Salaün
September 2019, 14 pages.
Hunting Superfluous Locks with Model Checking
VietAnh Nguyen, Wendelin Serwe, Radu Mateescu, and Eric Jenn
October 2019, 17 pages.
Compositional Verification of Concurrent Systems by Combining Bisimulations
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
October 2019, 26 pages.
Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving
Philippe Ledent, Anshul Paigwar, Alessandro Renzaglia, Radu Mateescu, and Christian Laugier
November 2019, 6 pages.
Asynchronous Testing of Synchronous Components in GALS Systems
Lina Marsso, Radu Mateescu, Ioannis Parissis, and Wendelin Serwe
December 2019, 18 pages.
On Modelbased Testing of GALS Systems
Lina Marsso
December 2019, 221 pages.
Autonomic Resilience of Distributed IoT Applications in the Fog
Umar Ozeer
December 2019, 184 pages.
Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and ObjectOriented Languages  The 4th Rewrite Engines Competition
Hubert Garavel, MohammadAli Tabikh, and ImadSeddik Arrada
April 2018, 28 pages.
TESTOR: A Modular Tool for OntheFly Conformance Test Case Generation
Lina Marsso, Radu Mateescu, and Wendelin Serwe
April 2018, 17 pages.
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
Hubert Garavel and Lina Marsso
April 2018, 47 pages.
Formal TLS Handshake Model in LNT
Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa
April 2018, 40 pages.
Automated Analysis of Industrial Workflowbased Models
Mario CortesCornax, Ajay Krishna, Adrian Mos, and Gwen Salaün
April 2018, 8 pages.
Modelchecking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits
Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, and Wendelin Serwe
May 2018, 9 pages.
Automated Verification of Automata Communicating via FIFO and Bag Buffers
Lakhdar Akroun and Gwen Salaün
June 2018, 20 pages.
Counterexample Simplification for Liveness Property Violation
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
June 2018, 16 pages.
Using LNT Formal Descriptions for ModelBased Diagnosis
Birgit Hofer, Radu Mateescu, Wendelin Serwe, and Franz Wotawa
August 2018, 8 pages.
Compositional Verification in Action
Hubert Garavel, Frédéric Lang, and Laurent Mounier
September 2018, 27 pages.
MCC'2017  The Seventh Model Checking Contest
Fabrice Kordon, Hubert Garavel, LomMessan Hillah, Emmanuel PaviotAdet, Loïg Jezequel, Francis HulinHubard, Elvio Gilberto Amparore, Marco Beccuti, Bernard Berthomieu, Hugues Evrard, Peter Gjøl Jensen, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Jirì Srba, Yann ThierryMieg, Jaco van de Pol, and Karsten Wolf
September 2018, 27 pages.
OntheFly Model Checking for Extended ActionBased Probabilistic Operators
Radu Mateescu and José Ignacio Requeno
October 2018, 24 pages.
Debugging of Behavioural Models using Counterexample Analysis
Gianluca Barbon
December 2018, 117 pages.
The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark
Hubert Garavel and Wendelin Serwe
April 2017, 41 pages.
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Hubert Garavel and Lina Marsso
April 2017, 55 pages.
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.
Debugging of Concurrent Systems using Counterexample Analysis
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
April 2017, 15 pages.
Asynchronous Synthesis Techniques for Coordinating Autonomous Managers in the Cloud
Rim Abid, Gwen Salaün, and Noël de Palma
May 2017, 34 pages.
The ContextAct@A4H RealLife Dataset of DailyLiving Activities  Activity Recognition using Model Checking
Paula Lago, Frédéric Lang, Claudia Roncancio, Claudia JiménezGuarín, Radu Mateescu, and Nicolas Bonnefond
June 2017, 14 pages.
VBPMN: Automated Verification of BPMN Processes
Ajay Krishna, Pascal Poizat, and Gwen Salaün
September 2017, 8 pages.
From LOTOS to LNT
Hubert Garavel, Frédéric Lang, and Wendelin Serwe
October 2017, 29 pages.
On the Most Suitable Axiomatization of Signed Integers
Hubert Garavel
December 2017, 16 pages.
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 FaultTolerant Routing Algorithm for a NetworkonChip 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.
OntheFly Model Checking for Extended ActionBased 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 Selfdeployment 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.
Stabilitybased Adaptation of Asynchronously Communicating Software
Carlos Canal and Gwen Salaün
June 2016, 16 pages.
Formal Framework for Modelling and Verifying Globally Asynchronous Locally Synchronous Systems
Fatma Jebali
September 2016, 225 pages.
MCC'2015  The Fifth Model Checking Contest
Fabrice Kordon, Hubert Garavel, Lom Messan Hillah, Emmanuel PaviotAdet, Loïg Jezequel, César Rodríguez, and Francis HulinHubard
September 2016, 11 pages.
Checking Business Process Evolution
Pascal Poizat, Gwen Salaun, and Ajay Krishna
October 2016, 18 pages.
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.
ModelBased Adaptation of Software Communicating via FIFO Buffers
Carlos Canal and Gwen Salaün
April 2015, 15 pages.
Using a Formal Model to Improve Verification of a CacheCoherent SystemonChip
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.
NestedUnit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets
Hubert Garavel
June 2015, 21 pages.
Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones
Hugues Evrard
July 2015, 199 pages.
Formal Methods for Functional Verification of CacheCoherent SystemonChip
Abderahman Kriouile
September 2015, 169 pages.
Asynchronous Coordination of Stateful Autonomic Managers in the Cloud
Rim Abid, Gwen Salaün, Noël de Palma, and Soguy MakKare 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.
Formal Analysis of a Hardware Dynamic Task Dispatcher with CADP
Etienne Lantreibecq and Wendelin Serwe
February 2014, 30 pages.
Reliable SelfDeployment 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 Modelbased Certification Framework for the EnergyBus Standard
Alexander GrafBrill, 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 FaultTolerant Routing Algorithm for a NetworkonChip
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.
PropertyDependent Reductions Adequate with DivergenceSensitive Branching Bisimilarity
Radu Mateescu and Anton Wijs
December 2014, 46 pages.
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 Selfconfiguration 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.
PIC2LNT: Model Tranformation for Model Checking and Applied PiCalculus
Radu Mateescu and Gwen Salaün
March 2013, 6 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, YvesStan 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 sharedmemory mutual exclusion protocols
Radu Mateescu and Wendelin Serwe
July 2013, 18 pages.
Formal Analysis of the ACE Specification for Cache Coherent SystemsonChip
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.
Checking the Realizability of BPMN 2.0 Choreographies
Pascal Poizat and Gwen Salaün
March 2012, 8 pages.
Verification of a Selfconfiguration 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 OntheFly Reduction Techniques
Radu Mateescu, Pascal Poizat, and Gwen Salaün
July 2012, 25 pages.
Largescale 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 OntheFly Computation of Weak TauConfluence
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.
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.
PropertyDependent Reductions for the Modal MuCalculus
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 Cosimulation of a Dynamic Task Dispatcher Circuit using CADP
Etienne Lantreibecq and Wendelin Serwe
August 2011, 16 pages.
Selfconfiguration 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.
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 SharedMemory 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 PiCalculus 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.
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 OntheFly Computation of Weak TauConfluence
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 FrontEnd 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.
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 ValuePassing 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 OntheFly 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 DiscreteTime Analysis of BPEL Web Services
Radu Mateescu and Sylvain Rampacek
June 2008, 15 pages.
Improved OntheFly 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 OntheFly Reduction Techniques
Radu Mateescu, Pascal Poizat, and Gwen Salaün
December 2008, 16 pages.
Formal Verification of CHP Specifications with CADP  Illustration on an Asynchronous NetworkonChip
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.
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 SmarandacheSturm,
and Gilles Stragier
March 2006, 5 pages.
Distributed OntheFly 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 OntheFly Resolution of AlternationFree 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.
Distributed Local Resolution of Boolean Equation Systems
Christophe Joubert and Radu Mateescu
February 2005, 8 pages.
BISIMULATOR: A Modular Tool for OntheFly 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 ModelChecking Approach
Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider
JulyAugust 2005, 6 pages.
TGV: Theory, Principles and Algorithms  A Tool for the Automatic Synthesis of Conformance Test Cases for NonDeterministic 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.
OntheFly State Space Reductions for Weak Equivalences
Radu Mateescu
September 2005, 10 pages.
EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and Onthefly 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.
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 TraceBased 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 OntheFly Equivalence Checking
Christophe Joubert and Radu Mateescu
September 2004, 15 pages.
Efficient OntheFly ModelChecking for Regular AlternationFree MuCalculus
Radu Mateescu and Mihaela Sighireanu
March 2003, 32 pages.
A Generic OntheFly Solver for AlternationFree 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.
OntheFly Verification using CADP
Radu Mateescu
June 2003, 5 pages.
Calculating TauConfluence 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.
Compositional Verification using SVL Scripts
Frédéric Lang
April 2002, 5 pages.
Local ModelChecking of Modal MuCalculus 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.
Parallel State Space Construction for ModelChecking
Hubert Garavel, Radu Mateescu, and Irina Smarandache
March 2001, 20 pages.
Specification and Verification of a Dynamic Reconfiguration Protocol for AgentBased 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.
Efficient Diagnostic Generation for Boolean Equation Systems
Radu Mateescu
January 2000, 23 pages.
Efficient OntheFly ModelChecking for Regular AlternationFree MuCalculus
Radu Mateescu and Mihaela Sighireanu
March 2000, 24 pages.
System Design of a CCNUMA Multiprocessor Architecture using Formal Specification, ModelChecking, CoSimulation, and Test Generation
Hubert Garavel, César Viho, and Massimo Zendri
November 2000, 36 pages.
Contribution à la Définition et à l'Implémentation du Langage ELOTOS
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.
ModelChecking 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 ELOTOS
Hubert Garavel and Mihaela Sighireanu
May 1998, 28 pages.
XTL: A MetaLanguage and Tool for Temporal Logic ModelChecking
Radu Mateescu and Hubert Garavel
July 1998, 10 pages.
Local ModelChecking of an AlternationFree ValueBased Modal MuCalculus
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.
Compositional State Space Generation from Lotos Programs
JeanPierre 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 IEEE1394 Serial Bus (``FireWire''): an Experiment with ELOTOS
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.
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
JeanClaude Fernandez, Claude Jard, Thierry Jéron, Laurence Nedelka, and César Viho
June 1996, 23 pages.
Using OntheFly Verification Techniques for the Generation of Test Suites
JeanClaude Fernandez, Claude Jard, Thierry Jéron, Laurence Nedelka, and César Viho
August 1996, 14 pages.
CADP: A Protocol Validation and Verification Toolbox
JeanClaude 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 ELOTOS
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.
A Local Checking Algorithm for Boolean Equation Systems
JeanClaude Fernandez and Laurent Mounier
March 1995, 15 pages.
On the Introduction of Gate Typing in ELOTOS
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
LouisPascal Tock
October 1995, 12 pages.
Formal Specification of a Framework for Groupware Development
Alain Kerbrat and Slim Ben Atallah
October 1995, 8 pages.
A LOTOS Specification of a "TransitNode"
Laurent Mounier
March 1994, 39 pages.
Reachable State Space Analysis of LOTOS programs
Alain Kerbrat
October 1994, 16 pages.
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
JeanClaude 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.
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
JeanClaude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, and Joseph Sifakis
May 1992, 14 pages.
``On the Fly'' Verification of Behavioural Equivalences and Preorders
JeanClaude Fernandez and Laurent Mounier
July 1991, 13 pages.
A Tool Set for Deciding Behavioral Equivalences
JeanClaude Fernandez and Laurent Mounier
August 1991, 20 pages.
Une Boîte à Outils pour la Vérification de Programmes LOTOS
JeanClaude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, and Joseph Sifakis
September 1991, 22 pages, in French.
An Implementation of an Efficient Algorithm for Bisimulation Equivalence
JeanClaude 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''
JeanClaude Fernandez and Laurent Mounier
November 1990, 16 pages.
Introduction au Langage LOTOS
Hubert Garavel
1990, 14 pages, in French.
Aldebaran User's Manual
JeanClaude Fernandez
January 1989, 7 pages.
Aldebaran: A Tool for Verification of Communicating Processes
JeanClaude 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.
ALDEBARAN : un Système de Vérification par Réduction de Processus Communicants
JeanClaude Fernandez
May 1988, 196 pages, in French.