Papers in Journals
-
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Logical Methods in Computer Science (LMCS), 2022. PDF
-
Chelsea Sidrane, Amir Maleki, Ahmed Irfan and Mykel J. Kochenderfer. OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems. The Journal of Machine Learning Research (JMLR), 2022. PDF
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Transactions on Computational Logic (TOCL), 2018. PDF
Conference Papers
-
Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi and Kristin Yvonne Rozier. The MoXI Model Exchange Tool Suite. International Conference on Computer-Aided Verification (CAV), 2024. PDF
-
Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stephane Graham-Lengrand and L. Kovacs. MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. International Joint Conference on Automated Reasoning (IJCAR), 2024. PDF
-
Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli and Moshe Y. Vardi. MoXI: An Intermediate Language for Symbolic Model Checking. International Symposium on Model Checking Software (SPIN), 2024. PDF
-
Ahmed Irfan, Sorawee Proncharoenwase, Zvonimir Rakamaric, Neha Rungta and Emina Torlak. Testing Dafny (Experience Paper). International Symposium on Software Testing and Analysis (ISSTA), 2022. PDF
-
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Noetzli, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli. Bit-Precise Reasoning via Int-Blasting. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2022. PDF
-
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonas, Marco Roveri, Roberto Sebastiani and Patrick Trentin. Optimization Modulo Non-Linear Arithmetic via Incremental Linearization. International Symposium on Frontiers of Combining Systems (FroCoS), 2021. PDF
-
Makai Mann, Amalee Wilson, Yoni Zohar, Lindsey Stuntz, Ahmed Irfan, Kristopher Brown, Caleb Donovick, Allison Guman, Cesare Tinelli and Clark Barrett. Smt-Switch: a Solver-agnostic C++ API for SMT Solving. International Conference on Theory and Applications of Satisfiability Testing (SAT), 2021. PDF
-
Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta and Clark Barrett. Pono: a Flexible and Extensible SMT-based Model Checker. International Conference on Computer-Aided Verification (CAV), 2021. PDF
-
Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, and Stefano Tonetta. Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. International Conference on Computer-Aided Verification (CAV), 2021. PDF
-
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2021. PDF Artifact
-
Ahmed Irfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel J. Kochenderfer, Baoluo Meng, James Lopez. Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance. Digital Avionics Systems Conference (DASC), 2020. PDF Slides
-
Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle D. Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, Clark Barrett. Parallelization Techniques for Verifying Neural Networks. Formal Methods in Computer-Aided Design (FMCAD), 2020. PDF
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Incremental Linearization: A Practical Approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2018. PDF
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. International Conference on Theory and Applications of Satisfiability Testing (SAT), 2018. PDF
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Satisfiability Modulo Transcendental Functions via Incremental Linearization. International Conference on Automated Deduction (CADE), 2017. PDF
-
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani. Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017. PDF
-
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani. Verilog2SMV: A Tool for Word-level Verification. Design, Automation and Test in Europe (DATE), 2016. PDF
Workshop Papers
-
Ahmed Irfan and Stephane Graham-Lengrand. Arrays Reasoning in MCSat. International Workshop on Satisfiability Modulo Theories (SMT), 2024. PDF
-
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani. Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. International. Workshop on Satisfiability Checking and Symbolic Computation (SC2), 2019. PDF
-
Alessandro Cimatti, Ahmed Irfan, Alberto Griggio, Marco Roveri, Roberto Sebastiani. A CEGAR-based Approach for Proving Invariant Properties of Transition Systems on Non-Linear Real Arithmetic. Workshop on Satisfiability Checking and Symbolic Computation (SC2), 2016. PDF
-
Ahmed Irfan, Davide Lanti, Norbert Manthey. Modern Cooperative Parallel SAT Solving. International Workshop on Pragmatics of SAT, 2013. PDF
Ph.D.
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. University of Trento and Fondazione Bruno Kessler, 2018. PDF