Cubing for Tuning
Haoze Wu, Clark Barrett, Nina Narodytska
Paper

Proof-Driven Clause Learning in Neural Network Verification
Omri Isac, Idan Refaeli, Haoze Wu, Clark Barrett, Guy Katz
Paper

Better Verified Explanations with Applications to Incorrectness and Out-of-Distribution Detection
Min Wu, Xiaofu Li, Haoze Wu, Clark Barrett
Paper

Per-Instance Subproblem Generation for Strategy Selection in SMT
Amalee Wilson, Nina Narodytska, Clark Barrett, and Haoze Wu
To appear in 2025 Formal Methods in Computer Aided Design (FMCAD'25)
Paper

Neural Network Verification is a Programming Language Challenge
Lucas C Cordeiro, Matthew L Daggitt, Julien Girard-Satabin, Omri Isac, Taylor T Johnson, Guy Katz, Ekaterina Komendantskaya, Augustin Lemesle, Edoardo Manino, Artjoms Šinkarovs, Haoze Wu
European Symposium on Programming (ESOP'25)
BibTeX Paper

Synthesis and Verification of String Stable Control for Interconnected Systems via Neural sISS Certificate
Jingyuan Zhou, Haoze Wu, Longhao Yan, Kaidi Yang
AI Verification in the Wild Workshop@ICLR'25 (VerifAI)
BibTeX Paper

Safe and Reliable Training of Learning-Based Aerospace Controllers
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto Ravaioli, Baoluo Meng, Michael Durling, Kerianne Hobbs, Milan Ganai, Tobey Shim, Guy Katz, Clark Barrett
AIAA DATC/IEEE 43rd Digital Avionics Systems Conference (DASC'24)
BibTeX Paper Code

Parallel Verification for delta-Equivalence of Neural Network Quantization
Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia, Clark Barrett
International Symposium on AI Verification (SAIV'24)
BibTeX Paper

Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark Barrett
Formal Methods in Computer-Aided Design (FMCAD'24)
BibTeX Paper

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark Barrett
International Conference on Computer Aided Verification (CAV'24)
BibTeX Paper Code

Lemur: Integrating Large Language Models in Automated Program Verification
Haoze Wu, Clark Barrett, Nina Narodytska
International Conference on Learning Representations (ICLR'24) (Oral Presentation at MATH-AI'23, BayLearn'24)
BibTeX Paper Code

Towards Efficient Verification of Quantized Neural Networks
Pei Huang, Haoze Wu, Yuting Yang, Ieva Daukantas, Min Wu, Yedi Zhang, Clark Barrett
AAAI Conference on Artificial Intelligence (AAAI'24) (Oral Presentation at the Safe, Robust, and Responsible AI track)
BibTeX Paper

VeriX: Towards Verified Explainability of Deep Neural Networks
Min Wu, Haoze Wu, Clark Barrett
Advances in neural information processing systems (NeurIPS'23)
BibTeX Paper Code

Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, Clark Barrett
Formal Methods in Computer-Aided Design (FMCAD'23) (Best paper nominee)
BibTeX Paper Code

Soy: An Efficient MILP Solver for Piecewise-Affine Systems
Haoze Wu, Min Wu, Dorsa Sadigh, Clark Barrett
IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'23)
BibTeX Paper Code

Convex Bounds on the Softmax Function with Applications to Robustness Verification
Dennis Wei, Haoze Wu, Min Wu, Pin-Yu Chen, Clark Barrett, Eitan Farchi
International Conference on Artificial Intelligence and Statistics (AISTATS'23)
BibTeX Paper Code

Toward Certified Robustness against Real-World Distribution Shifts
Haoze Wu*, Teruhiro Tagomori*, Alexander Robey*, Fengjun Yang*, Nikolai Matni, George Pappas, Hamed Hassani, Corina Pasareanu, Clark Barrett
2023 IEEE Conference on Secure and Trustworthy Machine Learning (SaTML'23)
BibTeX Paper
* denotes equal contribution.

Scalable Verification of GNN-based Job Schedulers
Haoze Wu, Clark Barrett, Mahmood Sharif, Nina Narodytska, Gagandeep Singh
Proceedings of the ACM on Programming Languages (OOPSLA'22)
BibTeX Paper Code

Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers
Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir, Clark Barrett
Formal Methods in Computer-Aided Design (FMCAD'22)
BibTeX Paper Code

On Optimizing Back-Substitution Methods for Neural Network Verification
Tom Zelazny, Haoze Wu, Clark Barrett, Guy Katz
Formal Methods in Computer-Aided Design (FMCAD'22)
BibTeX Paper Code

Efficient Neural Network Analysis with Sum-of-Infeasibilities
Haoze Wu, Aleksandar Zeljic, Guy Katz, Clark Barrett
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22)
BibTeX Paper Code

Global Optimization of Objective Functions Represented by ReLU Networks
Christopher A. Strong, Haoze Wu, Aleksandar Zeljić, Kyle D. Julian, Guy Katz, Clark Barrett, Mykel J. Kochenderfer
Journal of Machine Learning
BibTeX Paper Code

SAT-Solving in the Serverless Cloud
Alex Ozdemir*, Haoze Wu*, Clark Barrett
Formal Methods in Computer Aided Design (FMCAD'21)
BibTeX Paper Code
* denotes equal contribution.

An SMT-Based Approach for Verifying Binarized Neural Networks
Guy Amir, Haoze Wu, Clark Barrett, Guy Katz
Tools and Algorithms for the Construction and Analysis of Systems (TACAS'21)
BibTeX Paper Code

DeepCert: Verification of Contextually Relevant Robustness for Neural Network Image Classifiers
Colin Paterson, Haoze Wu, John Grese, Radu Calinescu, Corina S. Pasareanu, Clark Barrett
International Conference on Computer Safety, Reliability and Security (SafeComp'21)
BibTeX Paper Code

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, and James Lopez.
2020 AIAA/IEEE 39th Digital Avionics Systems Conference (DASC'20)
BibTeX Paper

Parallelization Techniques for Verifying Neural Networks
Haoze Wu, Alex Ozdemir, Aleksandar Zeljić, Ahmed Irfan, Kyle Julian, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, Clark Barrett
2020 Formal Methods in Computer Aided Design (FMCAD'20)
BibTeX Paper Code

G2SAT: Learning to Generate SAT Formulas
Jiaxuan You*, Haoze Wu*, Clark Barrett, Raghuram Ramanujan, Jure Leskovec
Advances in neural information processing systems (NeurIPS'19)
BibTeX Paper Code
* denotes equal contribution.

Learning to Generate Industrial SAT Instances
Haoze Wu, Raghuram Ramanujan
Twelfth Annual Symposium on Combinatorial Search (SoCS'19)
BibTeX Paper

The Marabou Framework for Verification and Analysis of Deep Neural Networks
Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L Dill, Mykel J Kochenderfer, Clark Barrett
International Conference on Computer Aided Verification (CAV'19)
BibTeX Paper Code

Improving SAT-solving with Machine Learning
Haoze Wu
ACM SIGCSE Technical Symposium on Computer Science Education (Student Research Competition)
BibTeX Paper