Approximations for Model Construction. - Aleksandar Zeljic; Christoph M. Wintersteiger; Philipp Rümmer (IJCAR, 2014)

Deciding Bit-Vector Formulas with mcSAT. - Aleksandar Zeljic; Christoph M. Wintersteiger; Philipp Rümmer (SAT, 2016)

An Approximation Framework for Solvers and Decision Procedures. - Aleksandar Zeljic; Christoph M. Wintersteiger; Philipp Rümmer (J. Autom. Reason., 2017)

From Machine Arithmetic to Approximations and back again: Improved SMT Methods for Numeric Data Types. - Aleksandar Zeljic (2017)

Exploring Approximations for Floating-Point Arithmetic Using UppSAT. - Aleksandar Zeljic; Peter Backeman; Christoph M. Wintersteiger; Philipp Rümmer (IJCAR, 2018)

Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction. - Peter Backeman; Philipp Rümmer; Aleksandar Zeljic (FMCAD, 2018)

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 003; Shantanu Thakoor; Haoze Wu 001; Aleksandar Zeljic; David L. Dill; Mykel J. Kochenderfer; et al. (CAV (1), 2019)

Parallelization Techniques for Verifying Neural Networks. - Haoze Wu 001; Alex Ozdemir; Aleksandar Zeljic; Kyle Julian; Ahmed Irfan; Divya Gopinath; Sadjad Fouladi; Guy Katz; Corina S. Pasareanu; Clark W. Barrett (FMCAD, 2020)

Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic. - Peter Backeman; Philipp Rümmer; Aleksandar Zeljic (Formal Methods Syst. Des., 2021)

Efficient Neural Network Analysis with Sum-of-Infeasibilities. - Haoze Wu 001; Aleksandar Zeljic; Guy Katz; Clark W. Barrett (TACAS (1), 2022)

Artifact for Paper Efficient Neural Network Analysis with Sum-of-Infeasibilities. - Haoze Wu 001; Aleksandar Zeljic; Guy Katz; Clark W. Barrett (Zenodo, 2022)

Global optimization of objective functions represented by ReLU networks. - Christopher A. Strong; Haoze Wu 001; Aleksandar Zeljic; Kyle D. Julian; Guy Katz; Clark W. Barrett; Mykel J. Kochenderfer (Mach. Learn., 2023)

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. - Haoze Wu 001; Omri Isac; Aleksandar Zeljic; Teruhiro Tagomori; Matthew L. Daggitt; Wen Kokke; Idan Refaeli; Guy Amir; Kyle Julian; Shahaf Bassan; Pei Huang 002; Ori Lahav 002; et al. (CAV (2), 2024)