Nicolas Amat

Nicolas Amat

PhD Student in Model Checking

LAAS-CNRS - Vertic 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.

Download my resumé.

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

Experience

 
 
 
 
 

Algorithmic Teacher (ADA language)

INSA Toulouse

Jan 2021 – Apr 2021 Toulouse, FRANCE
  • Tutorials, lab sessions and examination supervision.
 
 
 
 
 

Formal Methods Intern

LAAS-CNRS | INRIA

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

Embedded Software Intern

Arm Ltd.

Jun 2019 – Aug 2019 Cambridge, UK
  • A single C three month programming project related to the Arm Mali GPU software driver stack.
  • Running the Mali GPU driver on User-mode Linux (UML).
  • Modification of the driver to allow compatibility with UML.
  • Development of a 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.
  • Based on On the Expressive Completeness of Bernays-Schönfinkel-Ramsey 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