Aleksandar Zeljić

About

I am a computer scientist and a postdoc at Stanford at Center for Automated Reasoning at Stanford University and Stanford’s Center for AI Safety. I am supervised by Prof. Clark Barrett. My current work focuses on Marabou, a tool for deep neural network verification. My resume can be found here.

I hold a PhD from Department of Information Technology, Uppsala University. My PhD thesis was on SMT-style reasoning about machine arithmetic (floating-point and bit-vector arithmetics). I was supervised by Philipp Ruemmer, Christoph M. Wintersteiger and Wang Yi.

Research

My research interests include the following:

• Automated reasoning (SAT, SMT, Theorem proving)
• Formal verification and testing
• Verification of deep neural networks

My Projects:

• Marabou - a framework for verification of deep neural networks.
• UppSAT - implements an approximation-based framework for SMT solvers.
• mcBV - a model-constructing SMT solver for the theory of quantifier-free fixed-size bit-vectors.
• SmallFloats - prototype implementation of the approximation framework as a tactic within Z3 SMT solver.

Publications

• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic - P. Backeman, P. Rümmer, A. Zeljić in Formal Methods in System Design, 1-36, 2021

• Global Optimization of Objective Functions Represented by ReLU Networks - C. A. Strong, H. Wu, A. Zeljić, et al. in Machine Learning, 2021, https://doi.org/10.1007/s10994-021-06050-2

• Parallelization techniques for verifying neural networks - H. Wu, A. Ozdemir, A. Zeljić, et al. in 2020 Formal Methods in Computer Aided Design (FMCAD), 128-137, 18, 2020

• The Marabou framework for verification and analysis of deep neural networks - G. Katz, D. A. Huang, D. Ibeling, et al. in International Conference on Computer Aided Verification (CAV), 443-452, 177, 2019

• Bit-vector interpolation and quantifier elimination by lazy reduction - P. Backeman, P. Rümmer, A. Zeljić in 2018 Formal Methods in Computer Aided Design (FMCAD), 1-10

• Exploring Approximations for Floating-Point Arithmetic using UppSAT - A. Zeljić, P. Backeman, C. Wintersteiger, P. Rümmer in Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018), Springer, July 2018.

• An Approximation Framework for Solvers and Decision Procedures - A. Zeljić, C. Wintersteiger and P. Rümmer in Journal of Automated Reasoning, Springer, November 2016.

• Deciding Bit-Vector Formulas Using MCSAT - A. Zeljić, C. Wintersteiger and P. Rümmer in Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016).

• Approximations for Model Construction - A. Zeljić, C. Wintersteiger and P. Rümmer in Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Springer, July 2014. IJCAR Best Paper Award

Teaching

Over the years I have TA’d and/or organized the following courses:

• SAT/SMT Reading Group (2012)
• Programming Embedded Systems (2012-2016)
• Programming Theory (2012-2016, lecturer 2016)
• Automata and Logic in IT System Modelling (2014)
• Real-Time Systems (2015)
• Algorithms and Data Structures 1 (2017)
• Machine Learning (2018)
• Computer Architecture (2018)
• Advanced Topics in Formal Methods (2019, lecturer)

Service

PC member: VSSTE 2018, PAAR 2020, FOMLAS 2020, FOMLAS 2021

Reviewer: TCS, TACAS 2022, CAV 2021, JAR, TACAS 2020, IFM 2019, CADE 27, TACAS 2019, ICECCS 2018, IJCAR 2018, NFM 2017, TABLEAUX 2017, CADE 26, AAAI 17, FMCAD 2016, SMT 2016, IJCAR 2016, VMCAI 2016, FMCAD 2015, ATVA 2015, LCTES 2015, CAV 2015, FSEN 2015, TACAS 2015, SMT 2014, LPAR 19, SYNASC 2013, FMCAD 2013, ATVA 2013, IFM 2013, MEMOCODE 2012, ATVA 2012.