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
On the Complexity of Proving Polyhedral Reductions.
To appear in Fundamenta Informaticae (FI),
2024.
Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023.
To appear in TOOLympics 2023, Part III of the Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS),
2024.
PhD Thesis: A polyhedral Framework for Reachability Problems in Petri Nets.
INSA Toulouse,
2023.
A Toolchain to Compute Concurrent Places of Petri Nets.
ToPNoC,
2023.
Automated Polyhedral Abstraction Proving.
Petri Nets,
2023.
Kong: a Tool to Squash Concurrent Places.
Petri Nets,
2022.
On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets.
Petri Nets,
2021.
Master thesis: A New Approach for the Symbolic Model Checking of Petri nets.
University of Grenoble Alpes,
2020.
Softwares
.js-id-Model-Checking
Open science
Benchmark suites
- Model entitled “CryptoMiner”
Proposed for the Model Checking Contest 2023 - Model entitled “Murphy”
Proposed for the Model Checking Contest 2023 - Model entitled “PGCD”
Proposed for the Model Checking Contest 2023 - A QF-LIA Benchmark Suite from Polyhedral Reductions of Petri Nets
Proposed for the SMT-LIB repository and the SMT-COMP
Artifacts
- Artifact for TACAS 2022 Paper
Property Directed Reachability for Generalized Petri Nets - Artifact for FM 2023 Paper
SMPT: A Testbed for Reachability Methods in Generalized Petri Nets - Artifact for my PhD thesis
A polyhedral framework for reachability problems in Petri nets - Artifact for VMCAI 2024 Paper
Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
Talks
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
- International Conference on Formal Structures for Computation and Deduction (FSCD 2023), reviewer
- Science of Computer Programming (SCP), reviewer
- ACM Transactions on Embedded Computing Systems (TECS), reviewer
- International Journal on Software Tools for Technology Transfer (STTT), reviewer
- Workshop on Models for Formal Analysis of Real Systems (MARS2020), reviewer
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
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.
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
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
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
- nicolas [dot] amat [at] imdea [dot] org
- +34-91-101-2202
- Campus de Montegancedo s/n, Pozuelo de Alarcón, Madrid, 28223
- Office 246