|
A list of publications related to the CADP software is available here.
The list of publications of the former VASY team is available here.
Conferences and Workshops
Journals
- Design and Deployment of Expressive and Correct Web of Things Applications
Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün
ACM Transactions on Internet of Things 3(1):1-30, 2022.
| Full text: |
 |
- Verification of Distributed Systems via Sequential Emulation
Luca Di Stefano, Rocco De Nicola, and Omar Inverso
ACM Transactions on Software Engineering and Methodology 31(3):1-41, July 2022.
| Full text: |
|
- Models and Analysis for User-driven Reconfiguration of Rule-based IoT Applications
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün
Internet of Things 19:100515, August 2022.
| Full text: |
|
Conferences and Workshops
- Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles
Jean-Baptiste Horel, Christian Laugier, Lina Marsso, Radu Mateescu, Lucie Muller, Anshul Paigwar, Alessandro Renzaglia, and Wendelin Serwe
Proceedings of Design, Automation and Test in Europe - Autonomous Systems Design (DATE/ASD'2022), Antwerp, Belgium, March 14-18, 2022.
| Full text: |
|
- Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
Lina Marsso, Radu Mateescu, Lucie Muller, and Wendelin Serwe
Proceedings of the 5th Workshop on Models for Formal Analysis of Real Systems (MARS'2022), Munich, Germany, April 2, 2022.
| Full text: |
|
- From Static to Dynamic Analysis and Allocation of Resources for BPMN Processes
|
funded by Région Auvergne-Rhône-Alpes
|
 |
Francisco Durán, Yliès Falcone, Camilo Rocha, Gwen Salaün, and Ahang Zuo
Proceedings of the 14th International Workshop on Rewriting Logic and its Applications (WRLA'2022), Munich, Germany, April 2-3, 2022.
| Full text: |
|
- Counting Bugs in Behavioural Models using Counterexample Analysis
Irman Faqrizal and Gwen Salaün
Proceedings of the 10th International Conference on Formal Methods in Software Engineering (FormaliSE'2022), Pittsburgh, PA, May 18-22, 2022.
| Full text: |
|
- Probabilistic Model Checking of BPMN Processes at Runtime
|
funded by Région Auvergne-Rhône-Alpes
|
|
Yliès Falcone, Gwen Salaün, and Ahang Zuo
Proceedings of the 17th International Conference on integrated Formal Methods (iFM'2022), Lugano, Switzerland, June 7-10, 2022.
| Full text: |
|
- Runtime Enforcement for IEC 61499 Applications
Yliès Falcone, Irman Faqrizal, and Gwen Salaün
Proceedings of the 20th International Conference on Software Engineering and Formal Methods (SEFM'2022), Berlin, Germany, September 26-30, 2022.
| Full text: |
|
- Probabilistic Analysis of Industrial IoT Applications
Yliès Falcone, Irman Faqrizal, and Gwen Salaün
Proceedings of the 12th International Conference on the Internet of Things (IoT'2022), Delft, The Netherlands, November 7-10, 2022.
| Full text: |
|
- WEASY: A Tool for Modelling Optimised BPMN Processes
|
funded by Région Auvergne-Rhône-Alpes
|
|
Angel Contreras, Yliès Falcone, Gwen Salaün, and Ahang Zuo
Proceedings of the 18th International Conference on Formal Aspects of Component Software (FACS'2022), Oslo / online, Norway, November 10-11, 2022.
| Full text: |
|
- Debugging of BPMN Processes Using Coloring Techniques
Quentin Nivon and Gwen Salaün
Proceedings of the 18th International Conference on Formal Aspects of Component Software (FACS'2022), Oslo / online, Norway, November 10-11, 2022.
| Full text: |
|
Research Reports
Journals
- Quantifying the Similarity of Non-bisimilar Labelled Transition Systems
Gwen Salaün
Science of Computer Programming 202, 2021.
| Full text: |
|
- Debugging of Behavioural Models using Counterexample Analysis
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
IEEE Transactions on Software Engineering 47(6):1184-1197, 2021.
| Full text: |
|
- Compositional Verification of Concurrent Systems by Combining Bisimulations
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
Formal Methods in System Design 58:83-125, 2021.
| Full text: |
|
- Resource Provisioning Strategies for BPMN Processes: Specification and Analysis using Maude
Francisco Durán, Camilo Rocha, and Gwen Salaün
Journal of Logical and Algebraic Methods in Programming 123, 2021.
| Full text: |
|
Conferences and Workshops
- Seamless Reconfiguration of Rule-Based IoT Applications
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün
Proceedings of the 16th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS'2021), May 18-21, 2021.
| Full text: |
|
- R-MOZART: A Reconfiguration Tool for WebThings Applications
Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün
Proceedings of the 43rd ACM/IEEE International Conference on Software Engineering (ICSE'2021), Madrid, Spain (virtual event), May 25-28, 2021.
| Full text: |
|
- Efficient Algorithms for Three Reachability Problems in Safe Petri Nets
Pierre Bouvier and Hubert Garavel
Proceedings of the 42nd International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS'2021), virtual event, June 2021.
| Full text: |
|
|
Slides: |
|
- SAT-Competition Benchmarks Spawning from Concurrency Theory
Pierre Bouvier and Hubert Garavel
Proceedings of SAT Competition 2021 - Solver and Benchmark Descriptions, 2021.
- Consistent Substitution of Object in Rule-based IoT Applications
Gwen Salaün
Proceedings of the IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC'2021), Madrid, Spain (virtual event), July 12-16, 2021.
| Full text: |
|
- Semi-automated Modelling of Optimized BPMN Processes
|
funded by Région Auvergne-Rhône-Alpes
|
|
Yliès Falcone, Gwen Salaün, and Ahang Zuo
Proceedings of the IEEE International Conference on Services Computing (IEEE SCC'2021), virtual event, September 5-11, 2021.
| Full text: |
|
- Verifying Temporal Properties of Stigmergic Collective Systems Using CADP
Luca Di Stefano and Frédéric Lang
Proceedings of the 10th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'2021), Rhodes, Greece, October 25-29, 2021.
| Full text: |
|
- Business Process Models for Analysis of Industrial IoT Applications
Ajay Krishna and Gwen Salaün
Proceedings of the 11th International Conference on the Internet of Things (IoT'2021), St. Gallen, Switzerland, November 8-11, 2021.
| Full text: |
|
- Is CADP an Applicable Formal Method?
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
Proceedings of the 1st International Workshop on Applicable Formal Methods (αFM'2021), Beijing, China (virtual event), November 23, 2021.
| Full text: |
|
|
Slides: |
|
- Runtime Enforcement with Reordering, Healing, and Suppression
Yliès Falcone and Gwen Salaün
Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM'2021), virtual event, December 6-10, 2021.
| Full text: |
|
Research Reports
Journals and Proceedings Edited
Journals
Conferences and Workshops
- Using Model Checking to Identify Timing Interferences on Multicore Processors
Viet Anh Nguyen, Eric Jenn, Wendelin Serwe, Frédéric Lang, and Radu Mateescu
Proceedings of the 10th European Congress on Embedded Real Time Software and Systems (ERTS'2020), Toulouse, France, January 29-31, 2020.
| Full text: |
|
- MOZART: Design and Deployment of Advanced IoT Applications
Ajay Krishna, Michel Le Pallec, Alejandro Martinez, Radu Mateescu, and Gwen Salaün
Companion Proceedings of the Web Conference (WWW'2020), Taipei, Taiwan, April 20-24, 2020.
| Full text: |
|
|
Video: |
 |
- Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2020), Dublin, Ireland, 2020.
| Full text: |
|
- Specifying a Cryptographical Protocol in Lustre and SCADE
|
funded by Région Auvergne-Rhône-Alpes
|
|
Lina Marsso
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems (MARS'2020), Dublin, Ireland, 2020.
| Full text: |
|
- Modeling an Asynchronous Circuit Dedicated to the Protection Against Physical Attacks
Radu Mateescu, Wendelin Serwe, Aymane Bouzafour, and Marc Renaudin
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems (MARS'2020), Dublin, Ireland, 2020.
| Full text: |
|
- Analysis of the Runtime Resource Provisioning of BPMN Processes using Maude
Francisco Durán, Camilo Rocha, and Gwen Salaün
Proceedings of the 13th International Workshop on Rewriting Logic and its Applications (WRLA'2020), Dublin, Ireland, April 25-26, 2020.
| Full text: |
|
- Combining SLiVER with CADP to Analyze Multi-agent Systems
Luca Di Stefano, Frédéric Lang, and Wendelin Serwe
Proceedings of the 22nd IFIP WG 6.1 International Conference on Coordination Models and Languages (COORDINATION'2020), La Valetta, Malta, June 15-19, 2020.
| Full text: |
|
|
Slides: |
|
|
Video: |
|
- Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account
Pierre Bouvier, Hubert Garavel, Hernán Ponce de León
Proceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'2020), June 24-25, 2020.
| Full text: |
|
- The 2020 Expert Survey on Formal Methods
Hubert Garavel, Maurice ter Beek, and Jaco van de Pol
Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS'2020), Vienna, Austria, September 2-3, 2020.
| Full text: |
|
- Verification of a Failure Management Protocol for Stateful IoT Applications
Umar Ozeer, Gwen Salaün, Loïc Letondeur, François-Gaël Ottogalli, and Jean-Marc Vincent
Proceedings of the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS'2020), Vienna, Austria, September 2-3, 2020.
| Full text: |
|
- Clusters of Faulty States for Debugging Behavioural Models
Irman Faqrizal and Gwen Salaün
Proceedings of the 27th Asia-Pacific Software Engineering Conference (APSEC'2020), Singapore, December 1-4, 2020.
| Full text: |
|
- Automated Transition Coverage in Behavioural Conformance Testing
Lina Marsso, Radu Mateescu, and Wendelin Serwe
Proceedings of the 32nd IFIP International Conference on Testing Software and Systems (ICTSS'2020), Napoli, Italy, December 9-11, 2020.
| Full text: |
|
Research Reports
Theses
Journals
Book Chapters
- Reflections on Bernhard Steffen's Physics of Software Tools
Hubert Garavel and Radu Mateescu
Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays dedicated to Bernhard Steffen on the Occasion of His 60th Birthday, Limassol, Cyprus, June 2019.
| Full text: |
|
|
Slides: |
|
- Hunting Superfluous Locks with Model Checking
Viet-Anh Nguyen, Wendelin Serwe, Radu Mateescu, and Eric Jenn
From Software Engineering to Formal Methods and Tools, and Back: Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, Porto, Portugal, October 8, 2019.
| Full text: |
|
Conferences and Workshops
- Designing and Implementing Resilient IoT Applications in the Fog: A Smart Home Use Case
Umar Ozeer, Loïc Letondeur, François-Gaël Ottogalli, Gwen Salaün, and Jean-Marc Vincent
Proceedings of the 22nd Conference on Innovation in Clouds, Internet and Networks (ICIN'2019), Paris, France, February 19-21, 2019.
| Full text: |
|
- Debugging of Behavioural Models with CLEAR
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2019), Prague, Czech Republic, April 6-11, 2019.
| Full text: |
|
- TOOLympics 2019: An Overview of Competitions in Formal Methods
Ezio Bartocci, Dirk Beyer, Paul 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
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2019), Prague, Czech Republic, April 6-11, 2019.
| Full text: |
|
- The Rewrite Engines Competitions: A RECtrospective
Francisco Durán and Hubert Garavel
Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2019, Part III: TOOLympics), Prague, Czech Republic, April 6-11, 2019.
| Full text: |
|
|
Slides: |
|
- Visual Debugging of Behavioural Models
Gianluca Barbon, Vincent Leroy, Gwen Salaün, and Emmanuel Yah
Proceedings of the 41st ACM/IEEE International Conference on Software Engineering (ICSE'2019), Montréal, Canada, May 25-31, 2019.
| Full text: |
|
|
Video: |
|
- IoT Composer: Composition and Deployment of IoT Applications
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, and Gwen Salaün
Proceedings of the 41st ACM/IEEE International Conference on Software Engineering (ICSE'2019), Montréal, Canada, May 25-31, 2019.
| Full text: |
|
|
Video: |
|
- Rigorous Design and Deployment of IoT Applications
Ajay Krishna, Michel Le Pallec, Radu Mateescu, Ludovic Noirie, and Gwen Salaün
Proceedings of the 7th International Conference on Formal Methods in Software Engineering (FormaliSE'2019), Montréal, Canada, May 27, 2019.
| Full text: |
|
|
Slides: |
|
- Quantifying the Similarity of Non-bisimilar Labelled Transition Systems
Gwen Salaün
Proceedings of the 17th International Workshop on Coordination and Self-Adaptativeness of Software Applications (FOCLASA'2019), Oslo, Norway, September 16-20, 2019.
| Full text: |
|
- Compositional Verification of Concurrent Systems by Combining Bisimulations
Frédéric Lang, Radu Mateescu, and Franco Mazzanti
Proceedings of the 3rd World Congress on Formal Methods (FM'2019), Porto, Portugal, October 7-11, 2019.
| Full text: |
|
- Automated Composition, Analysis and Deployment of IoT Applications
Francisco Durán, Gwen Salaün, and Ajay Krishna
Proceedings of the 51st International Conference on Software Technology: Methods and Tools (TOOLS'2019), Innopolis, Russia, October 15-17, 2019.
| Full text: |
|
- Analysis of Resource Allocation of BPMN Processes
Francisco Durán, Camilo Rocha, and Gwen Salaün
Proceedings of the 17th International Conference on Service-Oriented Computing (ICSOC'2019), Toulouse, France, October 28-31, 2019.
| Full text: |
|
- Formal Validation of Probabilistic Collision Risk Estimation for Autonomous Driving
Philippe Ledent, Anshul Paigwar, Alessandro Renzaglia, Radu Mateescu, and Christian Laugier
Proceedings of the 9th IEEE International Conference on Cybernetics and Intelligent Systems, Robotics, Automation and Mechatronics (CIS-RAM'2019), Bangkok, Thailand, November 18-20, 2019.
| Full text: |
|
- Asynchronous Testing of Synchronous Components in GALS Systems
|
funded by Région Auvergne-Rhône-Alpes
|
|
Lina Marsso, Radu Mateescu, Ioannis Parissis, and Wendelin Serwe
Proceedings of the 15th International Conference on Integrated Formal Methods (iFM'2019), Bergen, Norway, December 2-6, 2019.
| Full text: |
|
|
Slides: |
|
Theses
Journals
- On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
Radu Mateescu and José Ignacio Requeno
Springer International Journal on Software Tools for Technology Transfer (STTT) 20(5):563-587, 2018.
| Full text: |
|
- Automated Verification of Automata Communicating via FIFO and Bag Buffers
Lakhdar Akroun and Gwen Salaün
Formal Methods in System Design 52(3):260-276, 2018.
| Full text: |
|
- Stochastic Analysis of BPMN with Time in Rewriting Logic
Francisco Durán, Camilo Rocha, and Gwen Salaün
Science of Computer Programming 168:1-17, 2018.
| Full text: |
|
- MCC'2017 - The Seventh Model Checking Contest
Fabrice Kordon, Hubert Garavel, Lom Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, Francis Hulin-Hubard, Elvio Amparore, Marco Beccuti, Bernard Berthomieu, Hugues Evrard, Peter Jensen, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Jirí Srba, Yann Thierry-Mieg, Jaco Van de Pol, and Karsten Wolf
Transactions on Petri Nets and Other Models of Concurrency XIII, LNCS 11090:181-209, 2018.
| Full text: |
|
Conferences and Workshops
- Automated Analysis of Industrial Workflow-based Models
Mario Cortes-Cornax, Ajay Krishna, Adrian Mos, and Gwen Salaün
Proceedings of the 33rd ACM/SIGAPP Symposium On Applied Computing (SAC'2018), Pau, France, April 9-13, 2018.
| Full text: |
|
|
Slides: |
|
- TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
|
funded by Région Auvergne-Rhône-Alpes
|
|
Lina Marsso, Radu Mateescu, and Wendelin Serwe
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2018), Thessaloniki, Greece, April 14-20, 2018.
| Full text: |
|
|
Slides: |
|
- Symbolic Specification and Verification of Data-aware BPMN Processes using Rewriting Modulo SMT
Francisco Durán, Camilo Rocha, and Gwen Salaün
Proceedings of the 12th International Workshop on Rewriting Logic and its Applications (WRLA'2018), Thessaloniki, Greece, April 14-15, 2018.
| Full text: |
|
- Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages - The 4th Rewrite Engines Competition
Hubert Garavel, Mohammad-Ali Tabikh, and Imad-Seddik Arrada
Proceedings of the 12th International Workshop on Rewriting Logic and its Applications (WRLA'2018), Thessaloniki, Greece, April 14-15, 2018.
| Full text: |
|
|
Slides: |
|
- A Formal TLS Handshake Model in LNT
|
funded by Région Auvergne-Rhône-Alpes
|
|
Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa
Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS/VPT'2018), Thessaloniki, Greece, April 20, 2018.
| Full text: |
|
|
Slides: |
|
- Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
Hubert Garavel and Lina Marsso
Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS/VPT'2018), Thessaloniki, Greece, April 20, 2018.
| Full text: |
|
|
Slides: |
|
- Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits
Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, and Wendelin Serwe
Proceedings of the 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'2018), Vienna, Austria, May 13-16, 2018.
| Full text: |
|
|
Slides: |
|
- Computing the Parallelism Degree of Timed BPMN Processes
Francisco Durán, Camilo Rocha, and Gwen Salaün
Proceedings of the 16th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems (FOCLASA'2018), associated with Software Technologies: Applications and Foundations (STAF'2018), Toulouse, France, June
16th, 2018.
| Full text: |
|
- Counterexample Simplification for Liveness Property Violation
Gianluca Barbon, Vincent Leroy, and Gwen Salaün
Proceedings of the 16th International Conference on Software Engineering and Formal Methods (SEFM'2018), Toulouse, France, June 27-29, 2018.
| Full text: |
|
- Using LNT Formal Descriptions for Model-Based Diagnosis
Birgit Hofer, Radu Mateescu, Wendelin Serwe, and Franz Wotawa
Proceedings of the 29th International Workshop on Principles of Diagnosis (DX'2018), Warsaw, Poland, August 27-30, 2018.
| Full text: |
|
|
Slides: |
|
- Compositional Verification in Action
Hubert Garavel, Frédéric Lang, and Laurent Mounier
Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS'2018), Maynooth, Ireland, September 3-4, 2018.
| Full text: |
|
- Resilience of Stateful IoT Applications in a Dynamic Fog Environment
Umar Ozeer, Xavier Etchevers, Loïc Letondeur, François-Gaël Ottogalli, Gwen Salaün, and Jean-Marc Vincent
Proceedings of the 15th EAI International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (MobiQuitous'2018), New York, USA, November 5-7, 2018
| Full text: |
|
Theses
Journals and Proceedings Edited
Journals
Book Chapters
- From LOTOS to LNT
Hubert Garavel, Frédéric Lang, and Wendelin Serwe
ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, Twente, The Netherlands, October 18, 2017.
| Full text: |
|
|
Slides: |
|
Conferences and Workshops
- Compatibility Flooding: Measuring Interaction of Services Interfaces
Meriem Ouederni, Uli Fahrenberg, Axel Legay, and Gwen Salaün
Proceedings of the Symposium on Applied Computing (SAC'2017), Marrakech, Morocco, April 3-7, 2017.
- 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: |
|
- 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: |
|
|
Slides: |
|
- 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: |
|
|
Slides: |
|
- 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: |
|
- On the Most Suitable Axiomatization of Signed Integers
Hubert Garavel
Proceedings of the 23rd International Workshop on Algebraic Development Techniques (WADT'2016), Gregynog, Wales, UK, September 21-24, 2016.
| Full text: |
|
Journals and Proceedings Edited
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: |
|
- 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: |
|
Book Chapters
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
|
|
|
