I am a computer scientist and I hold a PhD from Department of Information Technology, Uppsala University. My research focused 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. You can find my CV here.
My research interests include the following:
- Automated reasoning (SAT, SMT, Theorem proving)
- Formal verification and testing
- Machine learning
- 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.
Exploring Approximations for Floating-Point Arithmetic using UppSAT - A. Zeljic, P. Backeman, C. Wintersteiger, P. Rummer 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. Zeljic, C. Wintersteiger and P. Rummer in Journal of Automated Reasoning, Springer, November 2016.
Deciding Bit-Vector Formulas Using MCSAT - A. Zeljic, C. Wintersteiger and P. Rummer in Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016).
Approximations for Model Construction - A. Zeljic, C. Wintersteiger and P. Rummer in Proceedings of the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), Springer, July 2014. Best Paper Award
Over the course of my PhD I have been actively involved in teaching. I have TA’d and/or organized the following courses:
- SAT/SMT Reading Group (2012)
- Programming Embedded Systems (2012-2016)
- Programming Theory (2012-2016, course responsible 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).
PC member: VSSTE 2018
Sub-reviewer: 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.