I am a research scientist at ONERA (The French Aerospace Lab) in Toulouse. I am interested in theoretical computer science, with a special interest in the theory and applications of decision procedures for formal verification and robotics.

Previously I was a postdoctoral researcher at the IMDEA Software Institute, working on new solving techniques for Presburger arithmetic.

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é and visit my homepage.

My publications tracked by DBLP.

• Amat, N, Dal Zilio, S, Le Botlan, D. On the Complexity of Proving Polyhedral Reductions. Fundamenta Informaticae (FI).

• Amat, N, Bouvier, P, Garavel, H. A Toolchain to Compute Concurrent Places of Petri Nets. Petri Nets and Other Models of Concurrency (ToPNoC).
• Amat, N, Dal Zilio, S, Le Botlan, D. Leveraging polyhedral reductions for solving Petri net reachability problems. International Journal on Software Tools for Technology Transfer (STTT).

• Amat, N, Berthomieu, B, Dal Zilio, S. A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking. Fundamenta Informaticae (FI).

• Amat, N, Amparore, E, Berthomieu, B, Bouvier, P, Dal Zilio, S, Jensen, P, Jezequel, L, Kordon, F, Li, S, Paviot-Adet, E, Srba, J, Thierry-Mieg, Y, Wolf, K. Behind the Scene of the Model Checking Contest, Analysis of Results from 2018 to 2023. TOOLympics Challenge 2023.

• Amat, N, Le Botlan, D, Dal Zilio, S. Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024).

• Amat, N, Dal Zilio, S, Le Botlan, D. Automated Polyhedral Abstraction Proving. Application and Theory of Petri Nets and Concurrency (Petri Nets 2023).
• Amat, N, Dal Zilio, S. SMPT: A Testbed for Reachability Methods in Generalized Petri Nets. Formal Methods (FM 2023).

• Amat, N, Dal Zilio, S, Hujsa, T. Property Directed Reachability for Generalized Petri Nets. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022).
• Amat, N, Chauvet, L. Kong: A Tool to Squash Concurrent Places. Application and Theory of Petri Nets and Concurrency (Petri Nets 2022).

• Amat, N, Dal Zilio, S, Le Botlan, D. Accelerating the Computation of Dead and Concurrent Places Using Reductions. Model Checking Software (SPIN 2021).
• Amat, N, Berthomieu, B, Dal Zilio, S. On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. Application and Theory of Petri Nets and Concurrency (Petri Nets 2021).