Ahmed Irfan

According to our database, Ahmed Irfan authored at least 28 papers between 2013 and 2026.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2026

Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness (Long Tool Paper).

Aron Ricardo Perez-Lopez, Po-Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan, Clark W. Barrett

Proceedings of the Formal Methods - 27th International Symposium, 2026

2025

Prefix Trees Improve Memory Consumption in Large-Scale Continuous-Time Stochastic Models.

Landon Taylor, Joshua Jeppson, Ahmed Irfan, Lukas Buecherl, Chris J. Myers, Zhen Zhang

CoRR, December, 2025

Decision Heuristics in MCSat.

Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand

Proceedings of the Computer Aided Verification - 37th International Conference, 2025

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search.

Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand

Proceedings of the Automated Deduction - CADE 30, 2025

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

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

Proceedings of the Model Checking Software - 30th International Symposium, 2024

Arrays Reasoning in MCSat.

Ahmed Irfan, Stéphane Graham-Lengrand

Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), 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

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

The MoXI Model Exchange Tool Suite.

Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier

Proceedings of the Computer Aided Verification - 36th International Conference, 2024

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

Bit-Precise Reasoning via Int-Blasting.

Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark W. Barrett, Cesare Tinelli

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2022

Testing Dafny (experience paper).

Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, Emina Torlak

Proceedings of the ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18, 2022

2021

lazybvtoint at the SMT Competition 2020.

Yoni Zohar, Ahmed Irfan, Makai Mann, Andres Nötzli, Andrew Reynolds, Clark W. Barrett

CoRR, 2021

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays.

Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark W. Barrett

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 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

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems.

Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

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

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Parallelization Techniques for Verifying Neural Networks.

Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina S. Pasareanu, Clark W. Barrett

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

2019

Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization.

Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani

Proceedings of the 4th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2019

2018

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions.

Ahmed Irfan

PhD thesis, 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: A practical approach to satisfiability modulo nonlinear arithmetic and transcendental functions.

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani

Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization.

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2018, 2018

2017

Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF.

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Satisfiability Modulo Transcendental Functions via Incremental Linearization.

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani

Proceedings of the Automated Deduction - CADE 26, 2017

2016

Verilog2SMV: A tool for word-level verification.

Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani

Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition, 2016

2013

Modern Cooperative Parallel SAT Solving.

Norbert Manthey, Davide Lanti, Ahmed Irfan

Proceedings of the POS-13. Fourth Pragmatics of SAT workshop, 2013