Nicolas Amat

Nicolas Amat

PhD Student in Model Checking

LAAS-CNRS - VERTICS group

Biography

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

Interests

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

Education

  • 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

Publications

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

Teaching

2021/2022

  • 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

2020/2021

  • 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

Experience

 
 
 
 
 

Formal Methods Intern

LAAS-CNRS | INRIA

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.

Contact