Nicolas Amat

Nicolas Amat

PhD Student in Model Checking



I am a PhD student at LAAS-CNRS, in Toulouse. My research interests include model checking, Petri nets and SMT solving. I am currently working on new methods for taking advantage of Petri net reductions in combination with a SMT-based model-checker.

I am the PhD student representative of the Verification of Time Critical Systems (VERTICS) group, which develops new verification methods and tools for checking properties of critical systems.

Download my resumé (outdated).


  • Model Checking
  • Petri Nets
  • SAT/SMT Solving
  • Interactive Theorem Proving


  • PhD in Model Checking, 2020 - Present

    LAAS-CNRS - Toulouse, FRANCE

  • MoSIG - HECS, Master of Science, 2020 - 2019

    Univ. Grenoble Alpes - Grenoble, FRANCE

  • Engineering Degree, 2020 - 2017

    ENSIMAG - Grenoble, FRANCE


Kong: a Tool to Squash Concurrent Places. ICATPN, 2022.

PDF Project Slides DOI

Property Directed Reachability for Generalized Petri Nets. TACAS, 2022.

PDF Project Slides DOI

Master thesis. 2020.

PDF Slides



  • Advanced Time Models, Université Paul Sabatier, Toulouse, M2
  • Implementation techniques for discrete event systems, Université Paul Sabatier, Toulouse, M1
  • Discrete event systems, modeling and analysis, Université Paul Sabatier, Toulouse, M1


  • Algorithmic and Data Structures in ADA, INSA, Toulouse, L1

Intern Students

  • Louis Chauvet, INSA, Toulouse, L3
  • Sarah Moreau, INP, Toulouse, L2

Academic service

Distinctions & awards

Bronze Medal & 100% Confidence Award at the Model Checking Contest 2022

My tool, SMPT, won a bronze medal in the “reachability” category of the Model-Checking Contest 2022, an international competition of model-checking tools for the verification of concurrent systems. It also obtain the 100% confidence award.
See certificate

Petri Nets 2021 Teaser Video Award

For the teaser presentation of the paper: On the Combination of Polyhedral Abstraction and SMT-based Model Checking for Petri nets
See certificate

Persyval-lab Excellence Scholarship

Scholarship program for attracting exceptional candidates in the second year of one of its master’s degree related to the Persyval-lab disciplines.
See certificate



Formal Methods Intern


Feb 2020 – Jun 2020 Toulouse and Grenoble, FRANCE
  • Development of the SMPT model-checker for reachability properties on Petri nets.
  • Combination of polyhedral abstraction with SMT-based methods.
  • Development of Kong, a tool for the concurrent places problem.
  • Formalization of the $E$-abstraction equivalence.

Embedded Software Intern

Arm Ltd.

Jun 2019 – Aug 2019 Cambridge, UK
  • Running the Mali GPU driver on User-mode Linux (UML).
  • Modification of the driver to allow compatibility with UML.
  • Linux kernel patch to provide: Direct Memory Access (DMA), Device Tree.

Introduction to Laboratory Research

LIG - Grenoble Informatics Laboratory

Jan 2019 – Jun 2019 Grenoble, FRANCE
  • Formalization of Separation Logic using the Isabelle/HOL proof assistant.
  • Proof of formula transformation results of the separation logic.
  • Approximately 1,500 lines.

Crypto Developer Intern

IRIT - Toulouse Institute of Computer Science Research

May 2017 – Jun 2019 Toulouse, FRANCE
  • Open source project named XPIR : Private Information Retrieval for Everyone.
  • Private Information Retrieval software based on homomorphic encryption.
  • C++ and Python development.
  • Security improvement.