Grégoire SUTRE CNRS Research Fellow

About

Since October 2001, I hold a CNRS research fellow position at LaBRI, in the Modelling and Technologies for Verification Group of the Formal Methods and Models Team. My research concerns the formal modelling and algorithmic verification of complex systems. Applications that I've been involved with range from low-level systems code to high-level biological models. I am interested in both theoretical and practical aspects of verification.

Contact

Laboratoire Bordelais de Recherche en Informatique CNRS UMR 5800 Université de Bordeaux Building A30 351, cours de la Libération 33405 Talence Cedex FRANCE

Office 263 Phone +33 5 40 00 33 36 Fax +33 5 40 00 66 69 Email gregoire.sutre@labri.fr Web http://www.labri.fr/~sutre View my profile on LinkedIn

Research

Main topics

• Model-checking of safety properties.
• Infinite-state systems, distributed systems.
• Abstraction refinement.

Publications & talks

• Selected publications.
• Selected talks.
• List of publications from the DBLP Bibliography Server.

Software

• ICover — Petri Net Coverability Checker with Invariant-Based Pruning.
• McScM — Model Checker for Systems of Communicating fifo Machines.
• [see all]
• Berkeley Lazy Abstraction of Software Verification Tool.

Projects

• BraVAS (ANR/PRC, 2017–2023): Ideal-based Algorithms for VASSes and Well-Structured Systems.
• ReacHard (ANR/BLANC, 2011–2014): Taming Hard Reachability Problems for Counter Systems.
• VACSIM (ANR/INS, 2011–2015): Validation de la commande des systèmes critiques par couplage simulation et méthodes d'analyse formelle.
• [see all]
• FORWAL (GDR GPL): Formalismes et Outils pour la Vérification et la Validation.
• SPaCIFY (ANR/RNTL, 2007–2010): Model-Driven Engineering and Formal Methods for Critical Embedded Software.
• AVeriSS (ANR/ARA, 2007–2010): Automated Verification of Software Systems.
• Persée (ACI, 2003–2006): Symbolic techniques for the automatic verification of heterogeneous critical systems.
• MORSE (RNTL, 2003–2006): Méthodes et Outils pour la Vérification Formelle de Systèmes Intéropérables Embarqués critiques.

Teaching

Current courses

• Software Verification (2012–Now).

Former courses

• Formal Design with B (2001–2006, 2011-2012).
• Software Verification (2008–2010).

Professional Activities

Administration

• Member of the LaBRI Laboratory Council (02/2021–Now).

Seminar

• MV Seminar (Organizer, 09/2001–12/2005, 11/2012–12/2015).

Events

• Workshop RP'21 (Program Committee Member).
• Workshop GandALF'19 (Local Co-organizer).
• Workshop INFINITY'13 (Program Committee Member).
• Summer School MOVEP'12 (Program Committee Member).
• Workshop RP'12 (Local Co-organizer).
• Workshop VECOS'12 (Program Committee Member).
• [see all]
• Workshop VECOS'11 (Program Committee Member).
• Visite de l’ENS Cachan Bretagne à Bordeaux 2011 (Organizer).
• Workshop VECOS'10 (Program Committee Member).
• Summer School MOVEP'10 (Program Committee Member).
• Summer School VTSA'08 (Invited Speaker).
• Summer School MOVEP'08 (Steering Committee Member).
• Workshop AVOCS'06 (Program Committee Member).
• Summer School MOVEP'06 (Co-organizer).
• Spring School EJCACF'06 (Invited Speaker).

Students

Internship proposals

• Implémentation d'Algorithmes pour l'Analyse des SAVE de Dimension Deux. [html]

Master thesis proposals

• Counter-Boundedness for One-Dimensional Pushdown VASS. [html]

Current Ph.D. students

• Romain Delpy: Analysis and verification techniques for concurrent programs.
• Theo De Castro Pinto: Analyse automatisée de binaires appliquée à la recherche de vulnérabilités matérielles.

Former Ph.D. students

• Adrien Prevost: Vérification formelle par abstraction et raffinement incrémental : application à la certification de la sûreté de fonctionnement des postes d'enclenchement en phase d'étude.
• Thomas Geffroy (Ph.D. Univ. Bordeaux, 2017): Towards Efficient Tools for the Verification of Concurrent Systems. [theses]
• Farès Chucri (Ph.D. Univ. Bordeaux 1, 2012): Exploiting Model Structure in CEGAR Verification Method. [theses]
• Alexander Heußner (Ph.D. Univ. Bordeaux 1, 2011): Towards the verfication of safety properties for communicating infinite systems: decidability and abstraction refinement. [theses]
• Hayssam Soueidan (Ph.D. Univ. Bordeaux 1, 2009): Discrete event modeling and analysis for systems biology models. [theses]
• The Quang Tran (Ph.D. Univ. Bordeaux 1, 2009): Unfolding Based Verification of Concurrent Infinite-State Systems. [theses]

Former Post-docs

• Patrick Totzke (2014): Pushdown vector addition systems in small dimensions.
• M. Praveen (2013): On the boundedness problem for pushdown vector addition systems.
• Lorenzo Clemente (2012–2013): Reachability of communicating systems.
• Julien Forget (2010): Translation in AltaRica of the domain-specific modeling language Synoptic.

Extra

• Former developer for NetBSD and GRUB.
• [see all]
• The Raja Project: a ray-tracer written in Java.