default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDHubert Garavel
Person information
- affiliation: Inria Grenoble - Rhône-Alpes, CONVECS
- award (2023): ETAPS Test-of-Time Tool Award
- award (2023): ETAPS Test-of-Time Tool Award
- award (2021): Inria - Académie des Sciences - Dassault Systèmes Innovation Prize
- award (2011): Gay-Lussac Humboldt Prize
- award (1990): IBM France Young Scientist Award in Computer Science
2020 – today
- 2025
[j16]Maurice H. ter Beek, Rod Chapman
, Rance Cleaveland, Hubert Garavel, Rong Gu, Ivo ter Horst, Jeroen J. A. Keiren, Thierry Lecomte, Michael Leuschel, Kristin Yvonne Rozier, Augusto Sampaio, Cristina Seceleanu, Martyn Thomas, Tim A. C. Willemse, Lijun Zhang:
Formal Methods in Industry. Formal Aspects Comput. 37(1): 7:1-7:38 (2025)- 2024
- [c52]Pierre Bouvier, Hubert Garavel:
Identifying Duplicates in Large Collections of Petri Nets and Nested-Unit Petri Nets. Petri Nets 2024: 379-401 - [c51]Hubert Garavel, Holger Hermanns, David Parker:
Revisiting a Pioneering Concurrent Stochastic Problem: The Erlangen Mainframe. Principles of Verification (2) 2024: 46-74 - [c50]Hubert Garavel, Bas Luttik:
Four Formal Models of IEEE 1394 Link Layer. MARS@ETAPS 2024: 21-100 - 2023
- [j15]Nicolas Amat, Pierre Bouvier, Hubert Garavel:
A Toolchain to Compute Concurrent Places of Petri Nets. Trans. Petri Nets Other Model. Concurr. 17: 1-26 (2023) - 2022
- [c49]Hubert Garavel, Frédéric Lang:
Equivalence Checking 40 Years After: A Review of Bisimulation Tools. A Journey from Process Algebra via Timed Automata to Model Learning 2022: 213-265 - 2021
- [c48]Pierre Bouvier, Hubert Garavel:
Efficient Algorithms for Three Reachability Problems in Safe Petri Nets. Petri Nets 2021: 339-359 - [c47]Hubert Garavel, Frédéric Lang, Radu Mateescu, Wendelin Serwe:
Is CADP an Applicable Formal Method? AppFM@FM 2021: 1-11 - [i4]Hubert Garavel:
Proposal for Adding Useful Features to Petri-Net Model Checkers. CoRR abs/2101.05024 (2021) - [i3]Pierre Bouvier, Hubert Garavel:
The VLSAT-2 Benchmark Suite. CoRR abs/2110.06336 (2021) - 2020
- [c46]Pierre Bouvier, Hubert Garavel, Hernán Ponce de León:
Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. Petri Nets 2020: 3-23 - [c45]Hubert Garavel, Maurice H. ter Beek, Jaco van de Pol:
The 2020 Expert Survey on Formal Methods. FMICS 2020: 3-69 - [e3]Ansgar Fehnker, Hubert Garavel:
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems, MARS@ETAPS 2020, Dublin, Ireland, April 26, 2020. EPTCS 316, 2020 [contents] - [i2]Pierre Bouvier, Hubert Garavel:
The VLSAT-1 Benchmark Suite. CoRR abs/2011.11049 (2020)
2010 – 2019
- 2019
- [j14]Hubert Garavel:
Nested-unit Petri nets. J. Log. Algebraic Methods Program. 104: 60-85 (2019) - [c44]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, Akihisa Yamada:
TOOLympics 2019: An Overview of Competitions in Formal Methods. TACAS (3) 2019: 3-24 - [c43]Francisco Durán, Hubert Garavel:
The Rewrite Engines Competitions: A RECtrospective. TACAS (3) 2019: 93-100 - 2018
- [j13]Fabrice Kordon, Hubert Garavel, Lom-Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, Francis Hulin-Hubard, Elvio Gilberto Amparore, Marco Beccuti, Bernard Berthomieu, Hugues Evrard, Peter Gjøl Jensen, Didier Le Botlan, Torsten Liebke, Jeroen Meijer, Jirí Srba, Yann Thierry-Mieg, Jaco van de Pol, Karsten Wolf:
MCC'2017 - The Seventh Model Checking Contest. Trans. Petri Nets Other Model. Concurr. 13: 181-209 (2018) - [c42]Aymane Bouzafour, Marc Renaudin, Hubert Garavel, Radu Mateescu, Wendelin Serwe:
Model-Checking Synthesizable SystemVerilog Descriptions of Asynchronous Circuits. ASYNC 2018: 34-42 - [c41]Hubert Garavel, Radu Mateescu:
Reflections on Bernhard Steffen's Physics of Software Tools. Models, Mindsets, Meta 2018: 186-207 - [c40]Hubert Garavel, Frédéric Lang, Laurent Mounier:
Compositional Verification in Action. FMICS 2018: 189-210 - [c39]Hubert Garavel, Mohammad-Ali Tabikh, Imad-Seddik Arrada:
Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages - The 4th Rewrite Engines Competition. WRLA@ETAPS 2018: 1-25 - [c38]Hubert Garavel, Lina Marsso:
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm. MARS/VPT@ETAPS 2018: 41-87 - 2017
- [c37]Hubert Garavel, Frédéric Lang, Wendelin Serwe:
From LOTOS to LNT. ModelEd, TestEd, TrustEd 2017: 3-26 - [c36]Hubert Garavel, Lina Marsso:
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm. MARS@ETAPS 2017: 129-183 - [c35]Hubert Garavel, Wendelin Serwe:
The Unheralded Value of the Multiway Rendezvous: Illustration with the Production Cell Benchmark. MARS@ETAPS 2017: 230-270 - 2016
- [j12]Fabrice Kordon, Hubert Garavel, Lom-Messan Hillah, Emmanuel Paviot-Adet, Loïg Jezequel, César Rodríguez, Francis Hulin-Hubard:
MCC'2015 - The Fifth Model Checking Contest. Trans. Petri Nets Other Model. Concurr. 11: 262-273 (2016) - [c34]Hubert Garavel:
On the Most Suitable Axiomatization of Signed Integers. WADT 2016: 120-134 - 2015
- [j11]Hubert Garavel, Frédéric Lang, Radu Mateescu:
Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4-5): 337-392 (2015) - [j10]Hubert Garavel:
Revisiting sequential composition in process calculi. J. Log. Algebraic Methods Program. 84(6): 742-762 (2015) - [c33]Hubert Garavel:
Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets. Petri Nets 2015: 179-199 - 2014
- [c32]Alexander Graf-Brill, Holger Hermanns, Hubert Garavel:
A Model-Based Certification Framework for the EnergyBus Standard. FORTE 2014: 84-99 - 2013
- [j9]Hubert Garavel, Frédéric Lang, Radu Mateescu, Wendelin Serwe:
CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2): 89-107 (2013) - 2012
- [c31]Hubert Garavel, Radu Mateescu, Wendelin Serwe:
Large-scale Distributed Verification Using CADP: Beyond Clusters to Grids. PASM/PDMC 2012: 145-161 - 2011
- [c30]Hubert Garavel, Frédéric Lang, Radu Mateescu, Wendelin Serwe:
CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. TACAS 2011: 372-387 - 2010
- [c29]Nicolas Coste, Hubert Garavel, Holger Hermanns, Frédéric Lang, Radu Mateescu, Wendelin Serwe:
Ten Years of Performance Evaluation for Concurrent Systems Using CADP. ISoLA (2) 2010: 128-142
2000 – 2009
- 2009
- [j8]Hubert Garavel, Gwen Salaün, Wendelin Serwe:
On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. Sci. Comput. Program. 74(3): 100-127 (2009) - [c28]Jan Stöcker, Frédéric Lang, Hubert Garavel:
Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format. IFM 2009: 88-102 - [c27]Hubert Garavel, Claude Helmstetter, Olivier Ponsini, Wendelin Serwe:
Verification of an industrial SystemC/TLM model using LOTOS and CADP. MEMOCODE 2009: 46-55 - [c26]Hubert Garavel, Damien Thivolle:
Verification of GALS Systems by Combining Synchronous Languages and Process Calculi. SPIN 2009: 241-260 - 2008
- [c25]Nicolas Coste, Hubert Garavel, Holger Hermanns, Richard Hersemeule, Yvain Thonnart, Meriem Zidouni:
Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures. DATE 2008: 88-89 - [i1]Bernard Berthomieu, Hubert Garavel, Frédéric Lang, François Vernadat:
Verifying Dynamic Properties of Industrial Critical Systems Using TOPCASED/FIACRE. ERCIM News 2008(75) (2008) - 2007
- [c24]Hubert Garavel, Radu Mateescu, Frédéric Lang, Wendelin Serwe:
CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. CAV 2007: 158-163 - 2006
- [j7]Hubert Garavel, John Hatcliff:
Why you should definitely read this special section. Int. J. Softw. Tools Technol. Transf. 8(1): 1-3 (2006) - [j6]Hubert Garavel, Wendelin Serwe:
State space reduction for process algebra specifications. Theor. Comput. Sci. 351(2): 131-145 (2006) - [j5]Hubert Garavel, John Hatcliff:
TACAS 2003 Special Issue - Preface. Theor. Comput. Sci. 354(2): 169-172 (2006) - [c23]Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, Gilles Stragier:
DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. TACAS 2006: 445-449 - [c22]Hubert Garavel:
Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular. LIX 2006: 149-164 - 2004
- [c21]Hubert Garavel, Wendelin Serwe:
State Space Reduction for Process Algebra Specifications. AMAST 2004: 164-180 - [c20]Flávio Oquendo, Brian Warboys, Ronald Morrison, Régis Dindeleux, Ferdinando Gallo, Hubert Garavel, Carmen Occhipinti:
ArchWare: Architecting Evolvable Software. EWSA 2004: 257-271 - [c19]Hubert Garavel, Radu Mateescu:
SEQ.OPEN: A Tool for Efficient Trace-Based Verification. SPIN 2004: 151-157 - [c18]Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, Radu Mateescu:
Model Checking Genetic Regulatory Networks Using GNA and CADP. SPIN 2004: 158-163 - 2003
- [j4]Hubert Garavel, Stefania Gnesi, Ina Schieferdecker:
Special issue on the Fifth International Workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems, Berlin, April 3-4, 2000 - Selected papers. Sci. Comput. Program. 46(3): 195-196 (2003) - [c17]Frederic Tronel, Frédéric Lang, Hubert Garavel:
Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components. FMOODS 2003: 244-260 - [e2]Hubert Garavel, John Hatcliff:
Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science 2619, Springer 2003, ISBN 3-540-00898-5 [contents] - 2002
- [c16]Hubert Garavel, Frédéric Lang, Radu Mateescu:
Compiler Construction Using LOTOS NT. CC 2002: 9-13 - [c15]Hubert Garavel, Holger Hermanns:
On Combining Functional Verification and Performance Evaluation Using CADP. FME 2002: 410-429 - [c14]Hubert Garavel, Frédéric Lang:
NTIF: A General Symbolic Model for Communicating Sequential Processes with Data. FORTE 2002: 276-291 - [c13]Rance Cleaveland, Hubert Garavel:
Foreword. FMICS 2002: 211-213 - [e1]Rance Cleaveland, Hubert Garavel:
7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems, FMICS 2002, ICALP 2002 Satellite Workshop, Málaga, Spain, July 12-13, 2002. Electronic Notes in Theoretical Computer Science 66(2), Elsevier 2002 [contents] - 2001
- [j3]Hubert Garavel, César Viho, Massimo Zendri:
System design of a CC-NUMA multiprocessor architecture using formal specification, model-checking, co-simulation, and test generation. Int. J. Softw. Tools Technol. Transf. 3(3): 314-331 (2001) - [c12]Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, Noel De Palma:
Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. DAIS 2001: 229-242 - [c11]Hubert Garavel, Frédéric Lang:
SVL: A Scripting Language for Compositional Verification. FORTE 2001: 377-394 - [c10]Hubert Garavel, Radu Mateescu, Irina M. Smarandache:
Parallel State Space Construction for Model-Checking. SPIN 2001: 217-234
1990 – 1999
- 1999
- [c9]Hubert Garavel, Mihaela Sighireanu:
A Graphical Parallel Composition Operator for Process Algebras. FORTE 1999: 185-202 - 1998
- [c8]Hubert Garavel:
OPEN/CÆSAR: An OPen Software Architecture for Verification, Simulation, and Testing. TACAS 1998: 68-84 - 1997
- [j2]Hubert Garavel, Laurent Mounier:
Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Sci. Comput. Program. 29(1-2): 171-197 (1997) - 1996
- [c7]Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Laurent Mounier, Radu Mateescu, Mihaela Sighireanu:
CADP - A Protocol Validation and Verification Toolbox. CAV 1996: 437-440 - [c6]Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, Ferruccio Zulian:
Specification and Verification of the PowerScaleTM Bus Arbitration Protocol: An Industrial Experiment with LOTOS. FORTE 1996: 435-450 - [c5]Hubert Garavel, Mihaela Sighireanu:
On the Introduction of Exceptions in E-LOTOS. FORTE 1996: 469-484 - 1995
- [c4]Hubert Garavel:
On the introduction of gate typing in E-LOTOS. PSTV 1995: 283-298 - 1993
- [j1]Bernard Algayres, Veronigue Coelho, Laurent Doldi, Hubert Garavel, Yves Lejeune, Carlos Rodríguez:
VESAR: A Pragmatic Approach to Formal Specification and Verification. Comput. Networks ISDN Syst. 25(7): 779-790 (1993) - 1992
- [c3]Jean-Claude Fernandez, Hubert Garavel, Laurent Mounier, Anne Rasse, Carlos Rodríguez, Joseph Sifakis:
A Toolbox for the Verification of LOTOS Programs. ICSE 1992: 246-259 - 1990
- [c2]Hubert Garavel, Joseph Sifakis:
Compilation and verification of LOTOS specifications. PSTV 1990: 379-394
1980 – 1989
- 1989
- [b1]Hubert Garavel:
Compilation et vérification de programmes LOTOS. Joseph Fourier University, Grenoble, France, 1989 - [c1]Hubert Garavel:
Compilation of LOTOS Abstract Data Types. FORTE 1989: 147-162
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
[+][–] Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
[+][–] Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-03-04 21:17 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
