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

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

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