← Home

Publications

2025

2025
Decision Heuristics in MCSat
Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand
Computer-Aided Verification (CAV)
PDF
2025
Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand
Automated Deduction (CADE)
PDF
2025
Position Paper: A Case for Machine-Checked Verification of Circumvention Systems
Vitor Pereira, Ahmed Irfan, Vinod Yegneswaran, Nick Feamster, Prateek Mittal, Vitaly Shmatikov
Free and Open Communications on the Internet (FOCI)
PDF

2024

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
Computer-Aided Verification (CAV)
PDF
2024
Arrays Reasoning in MCSat
Ahmed Irfan, Stéphane Graham-Lengrand
Satisfiability Modulo Theories (SMT)
PDF
2024
MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács
International Joint Conference on Automated Reasoning (IJCAR)
PDF
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
Model Checking Software (SPIN)
PDF

2022

2022
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett
Logical Methods in Computer Science (LMCS)
PDF
2022
OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems
Chelsea Sidrane, Amir Maleki, Ahmed Irfan, Mykel J. Kochenderfer
Journal of Machine Learning Research (JMLR)
PDF
2022
Testing Dafny (Experience Paper)
Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamarić, Neha Rungta, Emina Torlak
Software Testing and Analysis (ISSTA)
PDF
2022
Bit-Precise Reasoning via Int-Blasting
Yoni Zohar, Ahmed Irfan, Makai Mann, Aina Niemetz, Andres Nötzli, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli
Verification, Model Checking, and Abstract Interpretation (VMCAI)
PDF

2021

2021
Optimization Modulo Non-Linear Arithmetic via Incremental Linearization
Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonáš, Marco Roveri, Roberto Sebastiani, Patrick Trentin
Frontiers of Combining Systems (FroCoS)
PDF
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 Barrett
Theory and Applications of Satisfiability Testing (SAT)
PDF
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 Barrett
Computer-Aided Verification (CAV)
PDF
2021
Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems
Sergio Mover, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Stefano Tonetta
Computer-Aided Verification (CAV)
PDF
2021
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
PDFArtifact

2020

2020
Towards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance
Ahmed Irfan, Kyle D. Julian, Haoze Wu, Clark Barrett, Mykel J. Kochenderfer, Baoluo Meng, James Lopez
Digital Avionics Systems Conference (DASC)
PDFSlides
2020
Parallelization Techniques for Verifying Neural Networks
Haoze Wu, Alex Ozdemir, Aleksandar Zeljić, Kyle D. Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, Clark Barrett
Formal Methods in Computer-Aided Design (FMCAD)
PDF

2019

2019
Lemmas for Satisfiability Modulo Transcendental Functions via Incremental Linearization
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Satisfiability Checking and Symbolic Computation (SC²)
PDF

2018

2018
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
ACM Transactions on Computational Logic (TOCL)
PDF
2018
Incremental Linearization: A Practical Approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
PDF
2018
Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Theory and Applications of Satisfiability Testing (SAT)
PDF

2017

2017
Satisfiability Modulo Transcendental Functions via Incremental Linearization
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Automated Deduction (CADE)
PDF
2017
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
PDF

2016

2016
A CEGAR-based Approach for Proving Invariant Properties of Transition Systems on Non-Linear Real Arithmetic
Alessandro Cimatti, Ahmed Irfan, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Satisfiability Checking and Symbolic Computation (SC²)
PDF
2016
Verilog2SMV: A Tool for Word-level Verification
Ahmed Irfan, Alessandro Cimatti, Alberto Griggio, Marco Roveri, Roberto Sebastiani
Design, Automation and Test in Europe (DATE)
PDF

2013

2013
Modern Cooperative Parallel SAT Solving
Ahmed Irfan, Davide Lanti, Norbert Manthey
Pragmatics of SAT (POS)
PDF

Theses

2018
Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
Ph.D. Thesis
University of Trento and Fondazione Bruno Kessler
PDF
2013
State-of-the-Art Cooperative Parallel SAT Solving
M.Sc. Thesis
Technische Universität Dresden
PDF
2012
Search Space Partitioning with Lookahead
M.Sc. Project Report
Technische Universität Dresden
PDF