Modern Cooperative Parallel SAT Solving. - Norbert Manthey; Davide Lanti; Ahmed Irfan (POS@SAT, 2013)

Verilog2SMV: A tool for word-level verification. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (DATE, 2016)

Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (CADE, 2017)

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (TACAS (1), 2017)

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SAT, 2018)

Incremental linearization: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (SYNASC, 2018)

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. - Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Marco Roveri; Roberto Sebastiani (ACM Trans. Comput. Log., 2018)

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. - Ahmed Irfan (2018)

Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization. - Ahmed Irfan; Alessandro Cimatti; Alberto Griggio; Marco Roveri; Roberto Sebastiani (SC-square@SIAM AG, 2019)

Parallelization Techniques for Verifying Neural Networks. - Haoze Wu 001; Alex Ozdemir; Aleksandar Zeljic; Kyle Julian; Ahmed Irfan; Divya Gopinath; Sadjad Fouladi; Guy Katz; Corina S. Pasareanu; Clark W. Barrett (FMCAD, 2020)

Pono: A Flexible and Extensible SMT-Based Model Checker. - Makai Mann; Ahmed Irfan; Florian Lonsing; Yahan Yang; Hongce Zhang; Kristopher Brown; Aarti Gupta; Clark W. Barrett (CAV (2), 2021)

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems. - Sergio Mover; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Stefano Tonetta (CAV (1), 2021)

Optimization Modulo Non-linear Arithmetic via Incremental Linearization. - Filippo Bigarella; Alessandro Cimatti; Alberto Griggio; Ahmed Irfan; Martin Jonás; Marco Roveri; Roberto Sebastiani; Patrick Trentin (FroCoS, 2021)

Smt-Switch: A Solver-Agnostic C++ API for SMT Solving. - Makai Mann; Amalee Wilson; Yoni Zohar; Lindsey Stuntz; Ahmed Irfan; Kristopher Brown; Caleb Donovick; Allison Guman; Cesare Tinelli; Clark W. Barrett (SAT, 2021)

lazybvtoint at the SMT Competition 2020. - Yoni Zohar; Ahmed Irfan; Makai Mann; Andres Nötzli; Andrew Reynolds 001; Clark W. Barrett (CoRR, 2021)

Testing Dafny (experience paper). - Ahmed Irfan; Sorawee Porncharoenwase; Zvonimir Rakamaric; Neha Rungta; Emina Torlak (ISSTA, 2022)

Bit-Precise Reasoning via Int-Blasting. - Yoni Zohar; Ahmed Irfan; Makai Mann; Aina Niemetz; Andres Nötzli; Mathias Preiner; Andrew Reynolds 001; Clark W. Barrett; Cesare Tinelli (VMCAI, 2022)

OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems. - Chelsea Sidrane; Amir Maleki; Ahmed Irfan; Mykel J. Kochenderfer (J. Mach. Learn. Res., 2022)

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. - Makai Mann; Ahmed Irfan; Alberto Griggio; Oded Padon; Clark W. Barrett (Log. Methods Comput. Sci., 2022)

The MoXI Model Exchange Tool Suite. - Chris Johannsen; Karthik Nukala; Rohit Dureja; Ahmed Irfan; Natarajan Shankar; Cesare Tinelli; Moshe Y. Vardi; Kristin Yvonne Rozier (CAV (1), 2024)

MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). - Thomas Hader; Daniela Kaufmann; Ahmed Irfan; Stéphane Graham-Lengrand; Laura Kovács (IJCAR (1), 2024)

Arrays Reasoning in MCSat. - Ahmed Irfan; Stéphane Graham-Lengrand (SMT@CAV, 2024)

MoXI: An Intermediate Language for Symbolic Model Checking. - Kristin Yvonne Rozier; Rohit Dureja; Ahmed Irfan; Chris Johannsen; Karthik Nukala; Natarajan Shankar; Cesare Tinelli; Moshe Y. Vardi (SPIN, 2024)

MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. - Thomas Hader; Daniela Kaufmann; Ahmed Irfan; Stéphane Graham-Lengrand; Laura Kovács (CoRR, 2024)

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. - Enrico Lipparini; Thomas Hader; Ahmed Irfan; Stéphane Graham-Lengrand (CADE, 2025)

Decision Heuristics in MCSat. - Thomas Hader; Ahmed Irfan; Stéphane Graham-Lengrand (CAV (3), 2025)