Hubert Garavel    home         cv        publications      talks      academic     editorship     music     photos

Scientific Publications

1989

Hubert Garavel. Compilation of LOTOS Abstract Data Types. In Son T. Vuong, editor, Proceedings of the 2nd International Conference on Formal Description Techniques (FORTE'89), Vancouver, BC, Canada, pages 147-162. North-Holland, December 1989.

1990

Hubert Garavel and Joseph Sifakis. Compilation and Verification of LOTOS Specifications. In L. Logrippo, R. L. Probert, and H. Ural, editors, Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (PSTV'90), Ottawa, Canada, pages 379-394. IFIP, North-Holland, June 1990.

1991

Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodriguez, and Joseph Sifakis. Une boîte à outils pour la vérification de programmes LOTOS. In Omar Rafiq, editor, Actes du Colloque Francophone pour l'Ingénierie des Protocoles (CFIP'91), Pau, France, pages 479-500, Paris, September 1991. Hermès.

Bernard Algayres, Véronique Coelho, Laurent Doldi, Hubert Garavel, Yves Lejeune, and Carlos Rodriguez. VESAR: Un Outil pour la Spécification et la Vérification Formelle de Protocoles. In Omar Rafiq, editor, Actes du Colloque Francophone pour l'Ingénierie des Protocoles (CFIP'91), Pau, France, pages 253-276, Paris, September 1991. Hermès.

1992

Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodriguez, and Joseph Sifakis. A Toolbox for the Verification of LOTOS Programs. In Lori A. Clarke, editor, Proceedings of the 14th International Conference on Software Engineering (ICSE'92), Melbourne, Australia, pages 246-259. ACM, May 1992.

1993

Bernard Algayres, Véronique Coelho, Laurent Doldi, Hubert Garavel, Yves Lejeune, and Carlos Rodriguez. VESAR: A Pragmatic Approach to Formal Specification and Verification. Computer Networks and ISDN Systems, volume 25, number 7, pages 779-790, February 1993.

Hubert Garavel and René-Pierre Hautbois. An Experiment with the Formal Description in LOTOS of the Airbus A340 Flight Warning Computer. In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, Proceedings of the 1st AMAST International Workshop on Real-Time Systems, Iowa City, IA, USA, November 1993.

Hubert Garavel and Philippe Turlier. CAESAR.ADT : un compilateur pour les types abstraits algébriques du langage LOTOS. In Rachida Dssouli and Gregor v. Bochmann, editors, Actes du Colloque Francophone pour l'Ingénierie des Protocoles (CFIP'93), Montréal, Canada, 1993.

1994

Hubert Garavel and René-Pierre Hautbois. Experimenting LOTOS in Aerospace Industry. In Teodor Rus and Charles Rattray, editors, Theories and Experiences for Real-Time System Development, volume 2 of Amast Series in Computing, chapter 11. World Scientific, 1994.

1995

Hubert Garavel. On the Introduction of Gate Typing in E-LOTOS. In Piotr Dembinski and Marek Sredniawa, editors, Proceedings of the 15th IFIP International Workshop on Protocol Specification, Testing and Verification (PSTV'95), Warsaw, Poland, IFIP, Chapman & Hall, June 1995.

1996

Hubert Garavel. An Overview of the Eucalyptus Toolbox. In Z. Brezocnik and T. Kapus, editors, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, pages 76-88. University of Maribor, Slovenia, June 1996.

Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Radu Mateescu, Laurent Mounier, and Mihaela Sighireanu. CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th Conference on Computer-Aided Verification (CAV'96), New Brunswick, New Jersey, USA, volume 1102 of Lecture Notes in Computer Science, pages 437-440. Springer, August 1996.

Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, and Ferruccio Zulian. Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS. In Reinhard Gotzhein and Jan Bredereke, editors, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'96), Kaiserslautern, Germany, pages 435-450. IFIP, Chapman & Hall, October 1996.

Hubert Garavel and Mihaela Sighireanu. On the Introduction of Exceptions in LOTOS. In Reinhard Gotzhein and Jan Bredereke, editors, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'96), Kaiserslautern, Germany, pages 469-484. IFIP, Chapman & Hall, October 1996.

1997

Hubert Garavel and Laurent Mounier. Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Science of Computer Programming, Special issue on Industrially Relevant Applications of Formal Analysis Techniques, Jan-Friso Groote and Martin Rem, editors, volume 29, number 1-2, pages 171-197, July 1997.

Hubert Garavel, Mark Jorgensen, Radu Mateescu, Charles Pecheur, Mihaela Sighireanu, and Bruno Vivien. CADP'97 - Status, Applications, and Perspectives. In Ignac Lovrek, editor, Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design, Zagreb, Croatia, June 1997.

1998

Hubert Garavel. OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing. In Bernhard Steffen, editor, Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), Lisbon, Portugal, volume 1384 of Lecture Notes in Computer Science, pages 68-84. Springer, March 1998.

Hubert Garavel and Mihaela Sighireanu. Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS. In Jan-Friso Groote, Bas Luttik and Jos van Wamel, editors, Proceedings of the 3rd International Workshop on Formal Methods for Industrial Critical Systems (FMICS'98), Amsterdam, The Netherlands, pages 187-230, May 1998. Invited lecture.

Radu Mateescu and Hubert Garavel. XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In Tiziana Margaria, editor, Proceedings of the International Workshop on Software Tools for Technology Transfer (STTT'98), Aalborg, Denmark, July 1998.

1999

Hubert Garavel and Mihaela Sighireanu. A Graphical Parallel Composition Operator for Process Algebras. In Jianping Wu, Qiang Gao, and Samuel T. Chanson, editors, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE/PSTV'99), Beijing, China, October 1999.

2000

Hubert Garavel, César Viho, and Massimo Zendri. System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation. Springer International Journal on Software Tools for Technology Transfer (STTT), volume 3, number 3, July 2001.

2001

Hubert Garavel, Radu Mateescu, and Irina Smarandache. Parallel State Space Construction for Model-Checking. In Matthew B. Dwyer, editor, Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'01), Toronto, Canada, volume 2057 of Lecture Notes in Computer Science, pages 217-234. Springer, May 2001.

Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, and Noel de Palma. Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. In Aleksander Laurentowski, Jacek Kosinski, Zofia Mossurska, and Radoslaw Ruchala, editors, Proceedings of the 3rd IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems (DAIS'01), Krakow, Poland, IFIP, Kluwer Academic Publishers, September 2001.

Hubert Garavel and Frédéric Lang. SVL: a Scripting Language for Compositional Verification. In Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee, editors, Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'01), Cheju Island, Korea, August 2001.

Hubert Garavel, Frédéric Lang, and Radu Mateescu. An overview of CADP 2001. Accepted for presentation at the Tools Day of CONCUR'02, Brno, Czech Republic, August 24, 2002 and published in Tiziana Margaria, editor, Tool Column of EASST Newsletter, volume 4, pages 13-24, August 2002. Also available as INRIA Technical Report 254, December 2001.

2002

Hubert Garavel, Frédéric Lang, and Radu Mateescu. Compiler Construction using LOTOS NT. In Nigel Horspool, editor, Proceedings of the 11th International Conference on Compiler Construction (CC'02), Grenoble, France, volume 2304 of Lecture Notes in Computer Science, pages 9-13. Springer, April 2002.

Hubert Garavel and Holger Hermanns. On Combining Functional Verification and Performance Evaluation using CADP. In Lars-Henrik Eriksson and Peter A. Lindsay, editors, Proceedings of the 11th International Symposium of Formal Methods Europe (FME'02), Copenhagen, Denmark, volume 2391 of Lecture Notes in Computer Science, pages 410-429. Springer, July 2002.

Hubert Garavel and Frédéric Lang. NTIF: A General Symbolic Model for Communicating Sequential Processes with Data. In Doron Peled and Moshe Vardi, editors, Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02), Houston, TX, USA, volume 2529 of Lecture Notes in Computer Science, pages 276-291. Springer, November 2002.

2003

Hubert Garavel. Défense et illustration des algèbres de processus. In Zoubir Mammeri, editor, Actes de l'Ecole d'été Temps Réel (ETR'03), Toulouse, France, September 2003. Invited paper.

Frédéric Tronel, Frédéric Lang, and Hubert Garavel. Compositional Verification using CADP of the ScalAgent Deployment Protocol for Software Components. In Uwe Nestmann and Perdita Stevens, editors, Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'03), Paris, France, volume 2884 of Lecture Notes in Computer Science, pages 244-260. Springer, November 2003.

2004

Hubert Garavel and Radu Mateescu. SEQ.OPEN: A Tool for Efficient Trace-Based Verification. In Susanne Graf and Laurent Mounier, editors, Proceedings of the 11th International SPIN Workshop on Model Checking of Software (SPIN'04), Barcelona, Spain, volume 2989 of Lecture Notes in Computer Science, pages 150-155. Springer, April 2004.

Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, and Radu Mateescu. Model Checking Genetic Regulatory Networks using GNA and CADP. In Susanne Graf and Laurent Mounier, editors, Proceedings of the 11th International SPIN Workshop on Model Checking of Software (SPIN'04), Barcelona, Spain, volume 2989 of Lecture Notes in Computer Science, pages 156-161. Springer, April 2004.

Flavio Oquendo, Brian Warboys, Ron Morrison, Régis Dindeleux, Ferdinando Gallo, Hubert Garavel, and Carmen Occhipinti. ArchWare: Architecting Evolvable Software. In Flavio Oquendo, Brian Warboys, and Ron Morrison, editors, Proceedings of the 1st European Workshop on Software Architectures (EWSA'04), St Andrews, Scotland, UK, volume 3047 of Lecture Notes in Computer Science, pages 257-271. Springer, May 2004. Invited paper.

Hubert Garavel and Wendelin Serwe. State Space Reduction for Process Algebra Specifications. In Charles Rattray, Savitri Maharaj, and Carron Shankland, editors Proceedings of the 10th International Conference on Algebraic Methodology and Software Methodology (AMAST'04), Stirling, Scotland, UK, July 2004.

2005

Hubert Garavel and Wendelin Serwe. State Space Reduction for Process Algebra Specifications. Theoretical Computer Science (TCS), volume 351, number 2, February 2006.

2006

Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier. DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. In Holger Hermanns and Jens Palberg, editors, Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), Vienna, Austria, volume 3920 of Lecture Notes in Computer Science, pages 445-449. Springer, March-April 2006.

2007

Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. In Werner Damm and Holger Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), Berlin, Germany, volume 4590 of Lecture Notes in Computer Science. Springer, July 2007.

Hubert Garavel. Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular. In Catuscia Palamidessi and Franck D. Valencia, editors, Proceedings of the LIX Colloquium on Emerging Trends in Concurrency Theory in honor of Professor Robin Milner, Ecole Polytechnique, France, November 13-15, 2006, volume 209 of Electronic Notes in Theoretical Computer Science, April 2008. Invited paper.

2008

Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gaufillet, Frédéric Lang, and François Vernadat. FIACRE: An Intermediate Language for Model Verification in the TOPCASED Environment. In Jean-Claude Laprie, Proceedings of the 4th European Congress on Embedded Real-Time Software (ERTS'08), Toulouse, France, January 2008.

Nicolas Coste, Hubert Garavel, Holger Hermanns, Richard Hersemeule, Yvain Thonnart, and Meriem Zidouni. Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures. In Proceedings of Design, Automation and Test in Europe (DATE'08), Munich, Germany, Special Session, March 2008.

2009

Hubert Garavel, Gwen Salaün, and Wendelin Serwe. On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP. Science of Computer Programming, volume 74, number 3, pages 100-127, January 2009.

Jan Stoecker, Frédéric Lang, and Hubert Garavel. Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. In Proceedings of the 7th International Conference on Integrated Formal Methods (IFM'09), Dusseldorf, Germany, February 2009.

Charles André, Mariano Belaunde, Bernard Berthomieu, Christian Brunette, Agusti Canals, Hubert Garavel, Susanne Graf, Frederic Lang, Vincent Mahé, Michel Nakhlé, Rémi Schnekenburger, Robert De Simone, Jean-Pierre Talpin, François Vernadat. Les résultats du projet OpenEmbeDD. In Actes de la conférence Neptune 2009, Paris, France, June 2009.

Hubert Garavel and Damien Thivolle. Verification of GALS Systems by Combining Synchronous Languages and Process Calculi. In Proceedings of the 16th International SPIN Workshop on Model Checking of Software (SPIN'09), Grenoble, France, June 2009.

Hubert Garavel, Claude Helmstetter, Olivier Ponsini, and Wendelin Serwe. Verification of an Industrial SystemC/TLM Model using LOTOS and CADP. In Proceedings of the 7th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'09), Cambridge, MA, USA, July 2009.

2010

Nicolas Coste, Hubert Garavel, Holger Hermanns, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. Ten Years of Performance Evaluation for Concurrent Systems Using CADP. In Proceedings of the 4th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation Part II (ISoLA'10), Heraclion, Crete, October 2010.

2011

Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), Saarbrücken, Germany, March 2011.

2012

Hubert Garavel, Radu Mateescu, and Wendelin Serwe. Large-Scale Distributed Verification using CADP: Beyond Clusters to Grids. In Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'12), London, United Kingdom, September 17, 2012.

2013

Hubert Garavel, Radu Mateescu, and Wendelin Serwe. Génération et manipulation d'espaces d'états distribués avec CADP: expériences sur Grid'5000. In Actes de la 21ème Conférence en Parallélisme, Architecture et Système (COMPAS'13), Grenoble, France, January 15-18, 2013.

Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. In Springer International Journal on Software Tools for Technology Transfer (STTT), volume 15, number 2, pages 89-107, 2013.

Hubert Garavel (editor) and Susanne Graf. Formal Methods for Safe and Secure Computer Systems. Bundesamt für Sicherheit in der Informationstechnik, BSI study 875, Bonn, Germany, 362 pages, December 2013.

2014

Alexander Graf-Brill, Holger Hermanns, and Hubert Garavel. A Model-based Certification Framework for the EnergyBus Standard. In Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'14), Berlin, Germany, voume 8461 of Lecture Notes in Computer Science, pages 84-99. Springer, June 2014.

2015

Hubert Garavel, Frédéric Lang, and Radu Mateescu. Compositional Verification of Asynchronous Concurrent Systems Using CADP. Acta Informatica, 61 pages, 2015.

Hubert Garavel. Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets. In Proceedings of the 36th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets'15), Bruxelles, Belgium, volume 9115 of Lecture Notes in Computer Science, pages 179-199. Springer, June 2015.

Hubert Garavel. Revisiting Sequential Composition in Process Calculi. Journal of Logical and Algebraic Methods in Programming, volume 84, number 6, pages 742-762, November 2015.

2016

Fabrice Kordon, Hubert Garavel, Lom Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, César Rodríguez, and Francis Hulin-Hubard. MCC'2015 - The Fifth Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), volume XI, pages 262-273, 2016.

2017

Hubert Garavel and Lina Marsso. A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm. In Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17), Uppsala, Sweden, April 2017. 55 pages.

Hubert Garavel and Wendelin Serwe. The Unheralded Value of Multiway Rendezvous: Illustration with the Production Cell Benchmark. In Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems (MARS'17), Uppsala, Sweden, April 2017. 41 pages.

Hubert Garavel, Frédéric Lang, and Wendelin Serwe. From LOTOS to LNT. In ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, volume 10500 of Lecture Notes in Computer Science, pages 3-26. Springer, October 2017.

Hubert Garavel. On the Most Suitable Axiomatization of Signed Integers. In Proceedings of the 23rd International Workshop on Algebraic Development Techniques (WADT'16), Gregynog, Wales, UK, volume 10644 of Lecture Notes in Computer Science, pages 120-134. Springer, December 2017.

2018

Hubert Garavel, Mohammad-Ali Tabikh, and Imad-Seddik Arrada. Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages - The 4th Rewrite Engines Competition. In Proceedings of the 12th International Workshop on Rewriting Logic and its Applications (WRLA'18), Thessaloniki, Greece, volume 11152 of Lecture Notes in Computer Science, pages 1-25. Springer, April 2018.

Hubert Garavel and Lina Marsso. Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. In 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'18), Thessaloniki, Greece, April 2018. 47 pages.

Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, and Wendelin Serwe. Model-checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits. In Proceedings of the 24th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC'18), Vienna, Austria, May 2018. 9 pages.

Fabrice Kordon, Hubert Garavel, Lom Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, Francis Hulin-Hubard, Elvio Amparore, Marco Beccuti, Bernard Berthomieu, Hugues Evrard, Peter G. Jensen, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Jiří Srba, Yann Thierry-Mieg, Jaco van de Pol, and Karsten Wolf. MCC'2017 - The Seventh Model Checking Contest. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), volume XIII, pages 181-209, 2018.

Hubert Garavel, Frédéric Lang, and Laurent Mounier. Compositional Verification in Action. In Proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS'18), Maynooth University, Ireland, volume 11119 of Lecture Notes in Computer Science, pages 189-210. Springer, September 2018.

2019

Hubert Garavel. Nested-Unit Petri Nets. Journal of Logical and Algebraic Methods in Programming, volume 104, pages 60-85, April 2019.

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. TOOLympics 2019: An Overview of Competitions in Formal Methods. In Part III of the Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), Prague, Czech Republic, volume 11429 of Lecture Notes in Computer Science, pages 3-24. Springer, April 2019.

Francisco Durán and Hubert Garavel. The Rewrite Engines Competitions: A RECtrospective. In Part III of the Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'19), Prague, Czech Republic, volume 11429 of Lecture Notes in Computer Science, pages 93-100. Springer, April 2019.

Hubert Garavel and Radu Mateescu. Reflections on Bernhard Steffen's Physics of Software Tools. In Models, Mindsets, Meta: The What, the How, and the Why Not?, volume 11200 of Lecture Notes in Computer Science, pages 186-207. Springer, June 2019.

2020

Pierre Bouvier, Hubert Garavel, and Hernán Ponce de Léon. Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. In Proceedings of the 41st International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'20), Paris, France, volume 12152 of Lecture Notes in Computer Science, pages 3-23. Springer, June 2020.

Hubert Garavel, Maurice H. ter Beek, and Jaco van de Pol. The 2020 Expert Survey on Formal Methods. In Proceedings of the 25th International Conference Formal Methods for Industrial Critical Systems (FMICS'20), Vienna, Austria, volume 12327 of Lecture Notes in Computer Science, pages 3-69. Springer, September 2020.

Pierre Bouvier and Hubert Garavel. The VLSAT-1 Benchmark Suite. INRIA Technical Report 510, November 2020.

Hubert Garavel. Proposal for Adding Useful Features to Petri-Net Model Checkers. Research Report, hal.inria.fr and Computer Research Repository arXiv abs/2101.05024, December 2020.

2021

Pierre Bouvier and Hubert Garavel. Efficient Algorithms for Three Reachability Problems in Safe Petri Nets. In Proceedings of the 42nd International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'21), Paris, France, volume 12734 of Lecture Notes in Computer Science, pages 339-359. Springer, June 2021.

Pierre Bouvier and Hubert Garavel. SAT-Competition Benchmarks Spawning from Concurrency Theory. In Proceedings of SAT Competition 2021 - Solver and Benchmark Descriptions, Report B-2021-1, pages 47-48, University of Helsinki, Department of Computer Science, July 2021.

Pierre Bouvier and Hubert Garavel. The VLSAT-2 Benchmark Suite. INRIA Technical Report 514, September 2021.

Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. Is CADP an Applicable Formal Method?. In Proceedings of the 1st International Workshop on Applicable Formal Methods (appFM'21), Bejing, China. November 2021.

2022

Hubert Garavel and Frédéric Lang. Equivalence Checking 40 Years After: A Review of Bisimulation Tools. In A Journey from Process Algebra via Timed Automata to Model Learning - Essays Dedicated to Frits Vaandrager on the Occasion of His 60th Birthday, volume 13560 of Lecture Notes in Computer Science, pages 213-265. Springer, September 2022.

2023

Nicolas Amat, Pierre Bouvier, and Hubert Garavel. A Toolchain to Compute Concurrent Places of Petri Nets. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC), volume XVII, pages 1-26, 2023.

2024

Hubert Garavel and Bas Luttik. Four Formal Models of IEEE 1394 Link Layer. In Proceedings of the 6th Workshop on Models for Formal Analysis of Real Systems (MARS 2024), Luxembourg, April 2024.

Pierre Bouvier and Hubert Garavel. Identifying Duplicates in Large Collections of Petri Nets and Nested-Unit Petri Nets. In Proceedings of the 45th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'24), Geneva, Switzerland, volume 14628 of Lecture Notes in Computer Science, pages 379-401. Springer, June 2024.

Maurice H. ter Beek, Rod Chapman, Rance Cleaveland, Hubert Garavel, Rong Gu, Ivo ter Horst, Jeroen J. A. Keiren, Thierry Lecomte, Michael Leuschel, Kristin Y. Rozier, Augusto Sampaio, Cristina Seceleanu, Martyn Thomas, Tim A. C. Willemse, and Lijun Zhang. Formal Methods in Industry. To appear in Formal Aspects of Computing, ACM.

Hubert Garavel, Holger Hermanns, and David Parker. Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe. To appear in Principles of Verification: Cycling the Probabilistic Landscape (Part II) - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, volume 15261 of Lecture Notes in Computer Science, pages 46-74. Springer, December 2024.

More...

Publications of the VASY team (1996-2011)

Publications of the CONVECS team (2012-now)

Publications related to the CADP software

French-Romanian contributions to the definition of E-LOTOS (1993-2002)