Nicolas Amat

Nicolas Amat

Postdoctoral researcher

IMDEA Software Institute

About me

I am currently a postdoctoral researcher at the IMDEA Software Institute, working on new solving techniques for Presburger arithmetic (under the supervision of Pierre Ganty and Alessio Mansutti).

I am interested in theoretical computer science, with a special interest in the theory and applications of decision procedures for formal verification.

I completed my PhD at LAAS-CNRS, where I worked on new methods for taking advantage of Petri net reductions with an SMT-based model checker.

Download my resumé.

Interests

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

Education

  • PhD in Model Checking, 2020 - 2023

    INSA Toulouse / LAAS-CNRS - Toulouse, FRANCE

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

    Univ. Grenoble Alpes - Grenoble, FRANCE

  • Engineering Degree, CS, 2017 - 2020

    ENSIMAG - Grenoble, FRANCE

Publications

My publications tracked by DBLP

A Toolchain to Compute Concurrent Places of Petri Nets. ToPNoC, 2023.

PDF Project DOI

Automated Polyhedral Abstraction Proving. Petri Nets, 2023.

PDF Project Slides DOI

Leveraging polyhedral reductions for solving Petri net reachability problems. STTT, 2022.

PDF Project DOI

Kong: a Tool to Squash Concurrent Places. Petri Nets, 2022.

PDF Project Slides DOI

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

PDF Project Slides DOI

Open science

Benchmark suites

Artifacts

Teaching

2022/2023

  • SAT/SMT Solving | PhD students & 2nd year graduate
    National School of Civil Aviation (ENAC), Toulouse, France
  • Advanced Time Models | 2nd year graduate
    Paul Sabatier University, Toulouse, France
  • Functional Programming in OCaml | 1st year graduate
    National Institute of Applied Sciences (INSA), Toulouse, France
  • Regular Expressions | 3rd year undergraduate
    National Institute of Applied Sciences (INSA), Toulouse, France
  • Algorithmic and Data Structures in ADA | 1st year undergraduate
    National Institute of Applied Sciences (INSA), Toulouse, France

2021/2022

  • Advanced Time Models | 2nd year graduate
    Paul Sabatier University
  • Discrete Event Systems, Modeling and Analysis | 1st year graduate
    Paul Sabatier University, Toulouse, France
  • Implementation Techniques for Discrete Event Systems | 1st year graduate
    Paul Sabatier University, Toulouse, France

2020/2021

  • Algorithmic and Data Structures in ADA | 1st year undergraduate
    National Institute of Applied Sciences (INSA), Toulouse, France

Intern Students

  • Louis Chauvet, INSA, Toulouse | 1st year graduate
    National Institute of Applied Sciences (INSA), Toulouse, France
  • Sarah Moreau, INP, Toulouse | 1st year graduate
    National Polytechnic Institute (INP), Toulouse, France

Academic service

Distinctions & awards

Bronze Medal at the Model Checking Contest 2023

My tool, SMPT, won a bronze medal in the “reachability” category of the Model-Checking Contest 2023, an international competition of model-checking tools for the verification of concurrent systems.
See certificate

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. It also obtains 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
I started developing SMPT, a model-checker for reachability problems in Petri nets. I proposed a first combination of polyhedral reductions with SMT-based methods and I was particularly interested in the concurrent places problem.
 
 
 
 
 

Embedded Software Intern

Arm Ltd.

Jun 2019 – Aug 2019 Cambridge, UK
I made a set of modifications to Arm’s Mali GPU driver to enable it to run on User-Mode Linux (UML), a compiled Linux kernel that can be executed in user-space as a simple program. I also proposed a Linux kernel patch to provide direct memory access (DMA) and devicetree compatibility on UML.
 
 
 
 
 

Introduction to Laboratory Research

LIG - Grenoble Informatics Laboratory

Jan 2019 – Jun 2019 Grenoble, FRANCE
I have carried out a formalization of separation logic using the Isabelle/HOL proof assistant, as well as the proof of formula rewriting results from a paper entitled “The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains”.
 
 
 
 
 

Crypto Developer Intern

IRIT - Toulouse Institute of Computer Science Research

May 2017 – Jun 2019 Toulouse, FRANCE
I have made some security enhancements to XPIR, an open source program that allows a user to secretly download an item from a database (the database server knows it has sent an item to the user, but does not know which one). Such a protocol is called Private Information Retrieval (PIR), and in XPIR’s case it is based on homomorphic encryption.

Contact