Pierre Bouvier

Contact

About me

I did my PhD thesis at Univ. Grenoble Alpes, in the CONVECS team of INRIA and LIG, and worked on formal methods under the supervision of Hubert Garavel and Radu Mateescu.

In 2019, I received an Engineering degree and a Research Master's degree in Computer Science and Applied Mathematics from École Nationale Supérieure d'Informatique et de Mathématiques Appliquées de Grenoble (ENSIMAG), a French "Grande École".

I have been an assistant engineer trainee at SAP Walldorf (Germany), within the Big Data - HANA Vora department, then a research intern within the CONVECS team.

Currently, I participate to the development of Kalray's next-generation high-performance storage solutions for data centers.

Publications

PhD thesis:

• Pierre Bouvier. Systèmes concurrents hiérarchiques : équivalence, analyse et structuration (Hierarchical Concurrent Systems: Equivalence, Analysis, and Structuring) - [theses.fr]. At Université Grenoble Alpes, Grenoble, France, October 2023.

Journal publication:

• Nicolas Amat, Pierre Bouvier and Hubert Garavel. A Toolchain to Compute Concurrent Places of Petri Nets. In Transactions on Petri Nets and Other Models of Concurrency XVII, LNCS 14150:1-26, 2023.

Conference papers:

• Nicolas Amat, Elvio Amparore, Bernard Berthomieu, Pierre Bouvier, Silvano Dal Zilio, Francis Hulin-Hubard, Peter Jensen, Loig Jezequel, Fabrice Kordon, Shuo Li, Emmanuel Paviot-Adet, Laure Petrucci, Jiri Srba, Yann Thierry-Mieg, and Karsten Wolf. Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023. In TOOLympics 2023, Part III of the Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23), Paris, France, April 2023 (to appear).
• Pierre Bouvier and Hubert Garavel. Efficient Algorithms for Three Reachability Problems in Safe Petri Nets. In Proceedings of the 42th Application and Theory of Petri Nets and Concurrency, PETRI NETS 2021, Paris, France, June 2021.
• Pierre Bouvier, Hubert Garavel and Hernán Ponce de León. Automatic Decomposition of Petri Nets into Automata Networks - A Synthetic Account. In Proceedings of the 41th Application and Theory of Petri Nets and Concurrency, PETRI NETS 2020, Paris, France, June 2020.

Technical reports:

• Pierre Bouvier. The VLSAT-3 Benchmark Suite. Inria Technical Report RT-0516, December 2021.
• Pierre Bouvier and Hubert Garavel. The VLSAT-2 Benchmark Suite. Inria Technical Report RT-0514, September 2021.
• Pierre Bouvier and Hubert Garavel. SAT-Competition Benchmarks Spawning from Concurrency Theory. In Proceedings of SAT Competition 2021 - Solver and Benchmark Descriptions, 2021.
• Pierre Bouvier and Hubert Garavel. The VLSAT-1 Benchmark Suite. Inria Technical Report RT-0510, November 2020.

Teaching

• 2020: Formal language theory 1
  L3 level, at the ENSIMAG engineering school (Grenoble INP) - 16.5h eq. TD
• 2020: Programming in C project - Development of a MIPS emulator
  M1 level, at the PHELMA engineering school (Grenoble INP) - 37h eq. TD
• 2020: Algorithms and data structures
  L3 level, at the ENSIMAG engineering school (Grenoble INP) - 33h eq. TD
• 2019: Programming in C project - Development of a MIPS emulator
  M1 level, at the PHELMA engineering school (Grenoble INP) - 31h eq. TD

Committees

• Member of the PhD student session of the École d'Été Temps Réel 2021, a summer school dedicated to young researchers from the real time community.
• Member of the model board of the Model Checking Contest 2021, 2022, 2023, and 2024, an international competition devoted to the evaluation of formal verification tools.

Talks

• Efficient Algorithms for Three Reachability Problems in Safe Petri Nets - [teaser video]
  Petri Nets 2021 conference, 24th June 2021
  
• Trois problèmes d'accessibilité dans les réseaux de Petri saufs
  MeFoSyLoMa seminar, LIP6, Paris, 11th June 2021
• Decomposition of Petri Nets into Automata Networks - A Synthetic Account
  Petri Nets 2020 conference, 25th June 2020

Data sets

The VLSAT benchmark suites, which are collections of logic formulas, to be used in scientific experiments and software competitions. These formulas have been obtained from the automatic conversion into Nested-Unit Petri Nets (NUPNs) of a large collection of Petri nets modelling real-life problems, such as communication protocols and concurrent systems.

Three collections are available at the moment:

• VLSAT-1: 100 SAT formulas having large numbers of models, dedicated to model counting
• VLSAT-2: 50 satisfiable and 50 unsatisfiable SAT formulas, dedicated to SAT solving
• VLSAT-3: 600 satisfiable and 600 unsatisfiable SMT formulas, dedicated to SMT solving

Software

• My GitHub account