About me
I am a PhD student at LAAS-CNRS, in France. My research interests include model-checking, SAT/SMT solving and logic methods in computer science. I am currently working on new methods for taking advantage of Petri net reductions in combination with a SMT-based model-checker.
I am also 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é.
Interests
- Model Checking
- SAT/SMT Solving
- Petri Nets
- Interactive Theorem Proving
Education
-
PhD in Model Checking, 2020 - Present
LAAS-CNRS - Toulouse, FRANCE
-
MoSIG - HECS, Master of Science, 2019 - 2020
Univ. Grenoble Alpes - Grenoble, FRANCE
-
Engineering Degree, 2017 - 2020
ENSIMAG - Grenoble, FRANCE
Publications
My publications tracked by DBLP
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.
2020.
Projects
.js-id-Model-Checking
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
- 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.
Embedded Software Intern
Arm Ltd.
- A three-month programming project related to the Arm Mali GPU software driver stack.
- Running the Mali GPU driver on User-mode Linux (UML).
- Development of Linux kernel patches.
Introduction to Laboratory Research
LIG - Grenoble Informatics Laboratory
- Formalization of Separation Logic using the Isabelle/HOL proof assistant.
- Proof of formula transformation results of the separation logic.
Crypto Developer Intern
IRIT - Toulouse Institute of Computer Science Research
- Private Information Retrieval software based on homomorphic encryption.
- C++ and Python development.
- Security improvement.
Contact
- namat [at] laas [dot] fr
- +33 5 61 33 63 63
- LAAS-CNRS, 7 Avenue du Colonel Roche, Toulouse, 31400
- Office A128c