2025
A Certified Proof Checker for Deep Neural Network Verification In Imandra
R. Desmartin*, O. Isac*, E. Komendantskaya, G. Passmore, K. Stark, G. Katz (* equal contribution)
Proc. 16th Int. Conf. on Interactive Theorem Proving (ITP), September 2025
Abstraction-Based Proof Production in Formal Verification of Neural Networks
Y. Elboher, O. Isac, G. Katz, T. Ladner, H. Wu
Proc. 8th Int. Symposium on AI Verification (SAIV), July 2025
Proof-Driven Clause Learning in Neural Network Verification
O. Isac*, I. Refaeli*, H. Wu, C. Barrett, G. Katz (* equal contribution)
2025
Neural Network Verification is a Programming Language Challenge
L. Cordeiro, M. Daggitt, J. Girard-Satabin, O. Isac, T. Johnson, G. Katz, E. Komendantskaya, A. Lemesle, E. Manino, A. Šinkarovs, H. Wu
Proc. 34th European Symposium on Programming (ESOP), May 2025
NLP Verification: Towards a General Methodology for Certifying Robustness
M. Casadio, T. Dinkar, E. Komendantskaya, L. Arnaboldi, O. Isac, M. L. Daggitt, G. Katz, V. Rieser, O. Lemon
European Journal of Applied Mathematics, 2025
2024
Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing
Y. Elboher*, R. Elsaleh*, O. Isac*, M. Ducoffe, A. Galametz, G. Povéda, R. Boumazouza, N. Cohen, G. Katz (* equal contribution)
Best of Session Award, Proc. 43rd Digital Avionics Systems Conf. (DASC), September 2024
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
H. Wu, O. Isac, A. Zeljić, T. Tagomori, M. Daggitt, W. Kokke, I. Refaeli, G. Amir, K. Julian, S. Bassan, P. Huang, O. Lahav, M. Wu, M. Zhang, E. Komendantskaya, G. Katz, C. Barrett
Proc. 36th Int. Conf. on Computer Aided Verification (CAV), July 2024
2023
Towards a Certified Proof Checker for Deep Neural Network Verification
R. Desmartin*, O. Isac*, G. Passmore, K. Stark, E. Komendantskaya, G. Katz (* equal contribution)
Best Short-Paper Award, Proc. 33rd Int. Symposium on Logic-based Program Synthesis and Transformation (LOPSTR), October 2023
DNN Verification, Reachability, and the Exponential Function Problem
O. Isac, Y. Zohar, C. Barrett, G. Katz
Proc. 34th Int. Conf. on Concurrency Theory (CONCUR), September 2023
ANTONIO: Towards a Systematic Method of Generating NLP Benchmarks for Verification
M. Casadio, L. Arnaboldi, M. L. Daggitt, O. Isac, T. Dinkar, D. Kienitz, V. Rieser, E. Komendantskaya
Proc. 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), July 2023
2022
Neural Network Verification with Proof Production
O. Isac, C. Barrett, M. Zhang, G. Katz
Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), October 2022