Pierre Bouvier

Contact

About me

I am a last-year PhD student at Univ. Grenoble Alpes, in the CONVECS team of INRIA and LIG.

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 am working on formal methods under the supervision of Hubert Garavel and Radu Mateescu.

Publications

• 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.

• 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, 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.

• 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