Ahmed Irfan

I am a Principal Research Scientist at Code Metal, working on neurosymbolic AI for code transpilation. My research interests include automated reasoning, SAT and SMT solving, formal methods, and model checking. I'm one of the developers of the Yices2 SMT solver and co-chair of FMCAD 2025. I previously worked on neural network verification.

Selected Publications

2026
Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness
Áron Ricardo Perez-Lopez, Po-Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan, Clark Barrett
Formal Methods (FM)
🏆 Best Tool Paper Award
PDF
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
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)
Pono — SMT-based model checkerpast
More past projects
BTOR2YICES — BTOR2 to Yices2 translator
CVC4 — SMT solverpast
Marabou — neural network verificationpast
MathSAT5 — SMT solverpast
nuXmv — symbolic model checkerpast
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