Ahmed Irfan

I work on automated reasoning, SAT and SMT solving, formal methods, model checking, and neurosymbolic AI. I'm one of the developers of the Yices2 SMT solver and co-chair of FMCAD 2025. I previously worked on neural network verification.

Publications

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
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
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
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
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

All publications →

Software

Yices2 — SMT solver (active developer)
BTOR2YICES — BTOR2 to Yices2 translator
Pono — SMT-based model checkerpast
CVC4 — SMT solverpast
Marabou — neural network verificationpast
MathSAT5 — SMT solverpast
nuXmv — symbolic model checkerpast
More past projects
Kratos — C software analyzerpast
LazyBV2Int — bit-vector SMT solverpast
Pcassco — parallel SAT solverpast
prophic3 — CEG prophecy for arrayspast
Simulink2SMV — Simulink to SMV translatorpast
Verilog2SMV — Verilog to SMV translatorpast

Service

Earlier service
  • PC Member, SBMF · SMT · VSTTE · TACAS-AE2023
  • PC Member, FMCAD2022
  • Co-organizer, NFM-AI-SAFETY2020
  • PC Member, NFM · PAAR · SC2 · TACAS-AE2020

Competitions

Earlier entries
  • CVC4, lazybv2int, Pono, Prophic3, ic3ia (SMT-COMP, HWMCC, CHC-COMP)2020
  • Cosa2 (HWMCC), MathSAT5 (SMT-COMP)2019
  • CLAS, Pcassco (SAT Competition)2014
  • Pcassco (SAT Competition)2013