|
A list of publications related to the CADP software is available here.
The list of publications of the former VASY team is available here.
Journals
Conferences and Workshops
- Debugging of Concurrent Systems using Counterexample Analysis
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
Proceedings of the 7th IPM International Conference on Fundamentals of Software Engineering FSEN'2017 (Tehran, Iran), April 26-28, 2017.
| Full text: |
 |
- The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark
Hubert Garavel and Wendelin Serwe
Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems MARS'2017 (Uppsala, Sweden), April 29, 2017.
| Full text: |
|
- A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Hubert Garavel and Lina Marsso
Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems MARS'2017 (Uppsala, Sweden), April 29, 2017.
| Full text: |
|
- Verifying Timed BPMN Processes Using Maude
Francisco Durán and Gwen Salaün
Proceedings of the 19th International Conference on Coordination Models and Languages COORDINATION'2017 (Neuchâtel, Switzerland), June 19-22, 2017.
| Full text: |
|
- The ContextAct@A4H Real-Life Dataset of Daily-Living Activities Activity Recognition using Model Checking
Paula Lago, Frédéric Lang, Claudia Roncancio, Claudia Jiménez-Guarín, Radu Mateescu, and Nicolas Bonnefond
Proceedings of the 10th International and Interdisciplinary Conference on Modeling and Using Context CONTEXT'2017 (Paris, France), June 20-23, 2017.
| Full text: |
|
|
Slides: |
|
- VBPMN: Automated Verification of BPMN Processes
Ajay Krishna, Pascal Poizat, and Gwen Salaün
Proceedings of the 13th International Conference on Integrated Formal Methods IFM'2017 (Torino, Italy), September 18-22, 2017.
| Full text: |
|
Journals
- Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications
Rim Abid, Gwen Salaün, and Noël de Palma
Science of Computer Programming, 117:1-16, 2016.
| Full text: |
|
- 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
Science of Computer Programming, 118:24-39, 2016.
| Full text: |
|
- Verification of EB3 specifications using CADP
Dimitris Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu
Formal Aspects of Computing, 28(1):145-178, 2016.
| Full text: |
|
- VerChor: A Framework for the Design and Verification of Choreographies
Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Lina Ye
IEEE Transactions on Services Computing 9(4):647-660, 2016.
| Full text: |
|
- Robust and Reliable Reconfiguration of Cloud Applications
Francisco Durán and Gwen Salaün
Journal of Systems and Software 122:524-537, 2016.
| Full text: |
|
- Formal Modelling and Verification of GALS Systems Using GRL and CADP
Fatma Jebali, Frédéric Lang, and Radu Mateescu
Formal Aspects of Computing 28(5):767-804, 2016.
| Full text: |
|
- Taking Arduino to the Internet of Things: the ASIP Programming Model
Gianluca Barbon, Michael Margolis, Filippo Palumbo, Franco Raimondi, and Nick Weldin
Computer Communications 89-90:128-140, 2016.
- 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
Transactions on Petri Nets and Other Models of Concurrency XI, LNCS 9930:262-273, 2016.
Conferences and Workshops
- DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
Hugues Evrard
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2016 (Eindhoven, The Netherlands), April 2-8, 2016.
| Full text: |
|
|
Slides: |
|
- Automated Analysis of Asynchronously Communicating Systems
Lakhdar Akroun, Gwen Salaün, and Lina Ye
Proceedings of the 23rd International SPIN Symposium on Model Checking of Software SPIN'2016 (Eindhoven, The Netherlands), April 7-8, 2016.
| Full text: |
|
- On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
Radu Mateescu and José Ignacio Requeno
Proceedings of the 23rd International SPIN Symposium on Model Checking of Software SPIN'2016 (Eindhoven, The Netherlands), April 7-8, 2016.
| Full text: |
|
|
Slides: |
|
- Stability-based Adaptation of Asynchronously Communicating Software
Carlos Canal and Gwen Salaün
Proceedings of the 14th International Conference on Software Engineering and Formal Methods SEFM'2016 (Vienna, Austria), July 4-8, 2016.
| Full text: |
|
- DAPA: Degradation-Aware Privacy Analysis of Android Apps
Gianluca Barbon, Agostino Cortesi, Pietro Ferrara, and Enrico Steffinlongo
Proceedings of the 12th International Workshop on Security and Trust Management STM'2016 (Heraklion, Crete, Greece), September 26-27, 2016.
- Checking Business Process Evolution
Pascal Poizat, Gwen Salaün, and Ajay Krishna
Proceedings of the 13th International Conference on Formal Aspects of Component Software FACS'2016 (Besançon, France), October 19-21, 2016.
| Full text: |
|
Theses
Journals and Proceedings Edited
Journals
Conferences and Workshops
- Debugging Process Algebra Specifications
Gwen Salaün and Lina Ye
Proceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation VMCAI'2015 (Mumbai, India), January 12-14, 2015.
| Full text: |
|
|
Slides: |
|
- Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes
Hugues Evrard and Frédéric Lang
Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing PDP'2015 (Turku, Finland), March 4-6, 2015.
| Full text: |
|
|
Slides: |
|
- Model-Based Adaptation of Software Communicating via FIFO Buffers
Carlos Canal and Gwen Salaün
Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering FASE'2015 (London, UK), April 13-17, 2015.
| Full text: |
|
- Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip
Abderahman Kriouile and Wendelin Serwe
Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2015 (London, UK), April 13-17, 2015.
| Full text: |
|
|
Slides: |
|
- Reasoning in Description Logics with Variables: Preliminary Results Regarding the EL Logic
Lakhdar Akroun, Lhouari Nourine, and Farouk Toumani
Proceedings of the 28th International Workshop on Description Logics DL'2015 (Athens, Greece), June 7-10, 2015.
| Full text: |
|
- Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets
Hubert Garavel
Proceedings of the 36th International Conference on Application and Theory of Petri Nets and Concurrency PETRI NETS'2015 (Brussels, Belgium), June 21-26, 2015.
| Full text: |
|
|
Slides: |
|
- Plasticity of User Interfaces: Formal Verification of Consistency
Raquel Oliveira, Sophie Dupuy-Chessa, and Gaëlle Calvary
Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'2015 (Duisburg, Germany), June 23-26, 2015.
| Full text: |
|
- Equivalence Checking for Comparing User Interfaces
Raquel Oliveira, Sophie Dupuy-Chessa, and Gaëlle Calvary
Proceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'2015 (Duisburg, Germany), June 23-26, 2015.
| Full text: |
|
- Asynchronous Coordination of Stateful Autonomic Managers in the Cloud
Rim Abid, Gwen Salaün, Noël de Palma, and Soguy Mak-Kare Gueye
Proceedings of the 12th International Symposium on Formal Aspects of Components and Systems FACS'2015 (Rio de Janeiro, Brazil), October 14-16, 2015.
| Full text: |
|
- Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
Wendelin Serwe
Proceedings of the 1st International Workshop on Models for Formal Analysis of Real Systems MARS'2015 (Suva, Fiji), November 23, 2015.
| Full text: |
|
|
Slides: |
|
Theses
Research Reports
Journals
Conferences and Workshops
- Reliable Self-Deployment of Cloud Applications
Xavier Etchevers, Gwen Salaün, Fabienne Boyer, Thierry Coupaye, and Noël De Palma
Proceedings of the 29th ACM Symposium on Applied Computing SAC'2014 (Gyeongju, Korea), March 24-28, 2014.
| Full text: |
|
|
Slides: |
|
- Comparator: A Tool for Quantifying Behavioural Compatibility
Meriem Ouederni, Gwen Salaün, Javier Cámara, and Ernesto Pimentel
Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering FASE'2014 (Grenoble, France), April 5-13, 2014.
| Full text: |
|
- A Model-Based Certification Framework for the EnergyBus Standard
Alexander Graf-Brill, Holger Hermanns, and Hubert Garavel
Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems FORTE'2014 (Berlin, Germany), June 3-6, 2014.
| Full text: |
|
|
Slides: |
|
- Modélisation et validation formelle de systèmes globalement asynchrones et localement synchrones
Fatma Jebali, Mouna Tka Mnad, Christophe Deleuze, Frédéric Lang, Radu Mateescu, and Ioannis Parissis
Actes des 13èmes Journées sur les Approches Formelles dans l'Assistance au Développement de Logiciels AFADL'2014 (Paris, France), June 11-12, 2014.
| Full text: |
|
|
Slides: |
|
- Formal Verification of UI using the Power of a Recent Tool Suite
Raquel Oliveira, Sophie Dupuy-Chessa, and Gaëlle Calvary
Proceedings of the 6th ACM SIGCHI Symposium on Engineering Interactive Computing Systems EICS'2014 (Rome, Italy), June 17-20, 2014.
| Full text: |
|
|
Poster: |
|
- Robust Reconfiguration of Cloud Applications
Francisco Duràn and Gwen Salaün
Proceedings of the 17th International ACM Sigsoft Symposium on Component-Based Software Engineering CBSE'2014 (Lille, France), June 30-July 3, 2014.
| Full text: |
|
|
Slides: |
|
- Quantifying the Parallelism in BPMN Processes using Model Checking
Radu Mateescu, Gwen Salaün, and Lina Ye
Proceedings of the 17th International ACM Sigsoft Symposium on Component-Based Software Engineering CBSE'2014 (Lille, France), June 30-July 3, 2014.
| Full text: |
|
|
Slides: |
|
- 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
Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2014 (Florence, Italy), September 11-12, 2014.
| Full text: |
|
|
Slides: |
|
- Adaptation of Asynchronously Communicating Software
Carlos Canal and Gwen Salaün
Proceedings of the 12th International Conference on Service Oriented Computing ICSOC'2014 (Paris, France), November 3-6, 2014.
| Full text: |
|
|
Slides: |
|
- GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems
Fatma Jebali, Frédéric Lang, and Radu Mateescu
Proceedings of the 16th International Conference on Formal Engineering Methods ICFEM'2014 (Luxembourg, Luxembourg), November 3-5, 2014.
| Full text: |
|
|
Slides: |
|
Research Reports
Journals and Proceedings Edited
Journals
- CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2):89-107, 2013.
| Full text: |
|
- 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
Assurances for Self-Adaptive Systems, Springer Verlag, 2013.
| Full text: |
|
- Composition and Abstraction of Logical Regulatory Modules: Application to Multicellular Systems
Nuño Mendes, Frédéric Lang, Yves-Stan Le Cornec, Radu Mateescu, Grégory Batt, and Claudine Chaouiya
Bioinformatics 29(6):749-757, 2013.
- 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
Innovations in Systems and Software Engineering, Springer Verlag, 9(2):105-117, 2013.
| Full text: |
|
- Model Checking and Performance Evaluation with CADP Illustrated on Shared-Memory Mutual Exclusion Protocols
Radu Mateescu and Wendelin Serwe
Science of Computer Programming 78(7):843-861, 2013.
| Full text: |
|
- Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
Frédéric Lang and Radu Mateescu
Logical Methods in Computer Science 9(4), 2013.
| Full text: |
|
- Efficient Optimization of Large Probabilistic Models
Simon Struck, Matthias Güdemann, and Frank Ortmeier
Journal of Systems and Software 86(10):2488-2501, 2013.
| Full text: |
|
Conferences and Workshops
- 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
Actes de la 21ème Conférence en Parallélisme, Architecture et Système COMPAS'2013 (Grenoble, France), January 15-18, 2013.
| Full text: |
|
|
Slides: |
|
- PIC2LNT: Model Transformation for Model Checking an Applied Pi-Calculus
Radu Mateescu and Gwen Salaün
Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2013 (Rome, Italy), March 16-24, 2013.
| Full text: |
|
|
Slides: |
|
- VerChor: A Framework for Verifying Choreographies
Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Alexandre Dumont
Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering FASE'2013 (Rome, Italy), March 16-24, 2013.
| Full text: |
|
|
Slides: |
|
- Formal Verification of Distributed Branching Multiway Synchronization Protocols
Hugues Evrard and Frédéric Lang
Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems 33rd FORTE / 15th FMOODS (Florence, Italy), June 3-6, 2013.
| Full text: |
|
|
Slides: |
|
- Verification of EB3 Specifications using CADP
Dimitris Vekris, Frédéric Lang, Catalin Dima, and Radu Mateescu
Proceedings of the 10th International Conference on Integrated Formal Methods IFM'2013 (Turku, Finland), June 10-14, 2013.
| Full text: |
|
- Analyse formelle du protocole ACE : cohérence de caches des systèmes sur puce
Abderahman Kriouile and Wendelin Serwe
Actes de l'École d'été Temps-Réel ETR'2013 (Toulouse, France), 26-30 August, 2013.
| Full text: |
|
|
Poster: |
|
- Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip
Abderahman Kriouile and Wendelin Serwe
Proceedings of the 18th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2013 (Madrid, Spain), September 23-24, 2013.
| Full text: |
|
|
Slides: |
|
- Verification of a Dynamic Management Protocol for Cloud Applications
Rim Abid, Gwen Salaün, Francesco Bongiovanni, and Noël De Palma
Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis ATVA'2013 (Hanoi, Vietnam), October 15-18, 2013.
| Full text: |
|
|
Slides: |
|
- Compatibility Checking for Asynchronously Communicating Software
Meriem Ouederni, Gwen Salaün, and Tevfik Bultan
Proceedings of the 10th International Symposium on Formal Aspects of Component Software FACS'2013 (Nanchang, China), October 28-30, 2013.
| Full text: |
|
|
Slides: |
|
- Predictability Analysis of Distributed Discrete Event Systems
Lina Ye, Philippe Dague, and Farid Nouioua
Proceedings of the 52nd IEEE Conference on Decision and Control CDC'2013 (Florence, Italy), December 10-13, 2013.
| Full text: |
|
Journals and Proceedings Edited
Journals
- Adaptation of Service Protocols Using Process Algebra and On-the-Fly Reduction Techniques
Radu Mateescu, Pascal Poizat, and Gwen Salaün
IEEE Transactions on Software Engineering 38(4):755-777, 2012.
| Full text: |
|
- Interactive Specification and Verification of Behavioral Adaptation Contracts
Javier Cámara, Gwen Salaün, Carlos Canal, and Meriem Ouederni
Information and Software Technology 54(7):701-723, 2012.
| Full text: |
|
- On Explicit Substitution with Names
Kristoffer H. Rose, Roel Bloo, and Frédéric Lang
Journal of Automated Reasoning 49(2):275-300, 2012.
- A Generic Framework for N-Protocol Compatibility Checking
Francisco Durán, Meriem Ouederni, and Gwen Salaün
Science of Computer Programming 77(7-8):870-886, 2012.
| Full text: |
|
- Sequential and Distributed On-the-Fly Computation of Weak Tau-Confluence
Radu Mateescu and Anton Wijs
Science of Computer Programming 77(10-11):1075-1094, 2012.
| Full text: |
|
- Structural Reconfiguration of Systems under Behavioral Adaptation
Carlos Canal, Javier Cámara, and Gwen Salaün
Science of Computer Programming 78(1):46-64, 2012.
| Full text: |
|
- Realizability of Choreographies using Process Algebra Encodings
Gwen Salaün, Tevfik Bultan, and Nima Roohi
IEEE Transactions on Services Computing 5(3):290-304, 2012.
| Full text: |
|
Conferences and Workshops
- CADP : une boîte à outils pour la conception et l'analyse de systèmes distribués
Hubert Garavel, Frédéric Lang, Radu Mateescu, Gwen Salaün, and Wendelin Serwe
Tutoriel présenté aux 11èmes Journées Francophones sur les Approches Formelles dans l'Assistance au Développement de Logiciels AFADL'2012 (Grenoble, France), January 11-13, 2012.
| Abstract: |
|
|
Slides: |
|
- Unifying Probabilistic and Traditional Formal Model Based Analysis
Matthias Güdemann, Michael Lipaczewski, Simon Struck, and Frank Ortmeier
Proceedings of the Dagstuhl Workshop on Model-Based Development of Embedded Systems MBEES'2012 (Dagstuhl, Germany), February 6-8, 2012.
| Full text: |
|
- 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
Proceedings of the 27th Symposium on Applied Computing SAC'2012 (Riva del Garda, Italy), March 26-30, 2012.
| Full text: |
|
|
Slides: |
|
- Checking the Realizability of BPMN 2.0 Choreographies
Pascal Poizat and Gwen Salaün
Proceedings of the 27th Symposium on Applied Computing SAC'2012 (Riva del Garda, Italy), March 26-30, 2012.
| Full text: |
|
|
Slides: |
|
- Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems
Frédéric Lang and Radu Mateescu
Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2012 (Talinn, Estonia), March 24 - April 1, 2012.
| Full text: |
|
|
Slides: |
|
- Trajectory Description Conception for Industrial Robots
Sergey Alatartsev, Matthias Güdemann, and Frank Ortmeier
Proceedings of the 7th German Conference on Robotics ROBOTIK'2012 (Munich, Germany), May 21-22, 2012.
| Full text: |
|
- CADP: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, Gwen Salaün, and Wendelin Serwe
Tutorial presented at the 18th International Symposium on Formal Methods FM'2012 (Paris, France), August 27-31, 2012.
| Abstract: |
|
|
Slides: |
|
- Large-Scale Distributed Verification using CADP: Beyond Clusters to Grids
Hubert Garavel, Radu Mateescu, and Wendelin Serwe
Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation PDMC'2012 (London, UK), September 17, 2012.
| Full text: |
|
|
Slides: |
|
- Counterexample Guided Synthesis of Monitors for Realizability Enforcement
Matthias Güdemann, Gwen Salaün, and Meriem Ouederni
Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis ATVA'2012 (Trivandrum, Kerala), October 5-6, 2012.
| Full text: |
|
|
Slides: |
|
- Multi-Objective Optimization of Formal Specifications
Simon Struck, Michael Lipaczewski, Frank Ortmeier, and Matthias Güdemann
Proceedings of the 14th IEEE International High Assurance Systems Engineering Symposium HASE'2012 (Omaha, Nebraska, USA), October 25-27, 2012.
| Full text: |
|
Journals and Proceedings Edited
Miscellaneous
|
|
|
