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

My publications tracked by DBLP.

• 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, 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).

• Amat, N, Dal Zilio, S, Le Botlan, D. On the Complexity of Proving Polyhedral Reductions. Submitted.
• 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 2023, Part III of the Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023) (to appear)