I am an Assistant Professor of Computer Science at the School of Computing and Information Systems at Singapore Management University. Previously, I obtained my PhD in 2023 at the Institute of Science and Technology Austria (ISTA), where I was fortunate to be supervised by Krishnendu Chatterjee and Petr Novotný. For my PhD work, I received the Outstanding PhD Thesis award at ISTA. I also received the Outstanding Scientific Achievement 2023 award at ISTA, together with my collaborator Mathias Lechner, for our work on developing the first framework for certified learning and formal verification of neural controllers in stochastic dynamical systems. Before that, I obtained bachelor’s and master’s degrees in mathematics at the University of Cambridge.

You can reach me at dzikelic@smu.edu.sg.

Openings

I have multiple openings for motivated PhD students, interns, and visiting PhD/master/undergrad students, to work with me on topics related to formal methods, trustworthy AI or program analysis. Please see this page if interested.

Research Interests

My research is concerned with helping programmers ensure that AI and software systems are correct, safe, and trustworthy. To achieve this, I study Formal Methods and their applications to Trustworthy AI and Safe Autonomy, as well as Program Analysis and Verification. The long term goal of my work is to advance the theory and automation of formal methods for trustworthy AI and software, especially in the presence of probabilistic uncertainty. My work is concerned with both theoretical aspects of formal reasoning about probabilistic systems, as well as the development of automated methods to help programmers build correct AI and software systems in practice. My current research interests include:

1. Trustworthy AI and Safe Autonomy
   • Learning-enabled control and safe reinforcement learning (NeurIPS23, ATVA23, TACAS23, AAAI23, AAAI22)
   • Formal verification and synthesis in Markov models (IJCAI24a, IJCAI24b, CAV23, FSTTCS22)
   • Formal verification of learned systems (e.g. neural networks) (AAAI23, NeurIPS21, AAAI21)
2. Program Analysis and Verification
   • Probabilistic programs (PLDI24, OOPSLA24, FAC23, CAV22, POPL17)
   • Numerical programs (FM24, PLDI22, PLDI21)
3. Broader perspective and applications of probabilistic system verification:
   • Bidding games on graphs (ECAI23, AAAI23, SODA21, JCSS21)
   • Blockchain protocol analysis (PODC24)

News

• October 2024. Distinguished Reviewer Award at SETTA 2024.

• September 2024. Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs is awarded a Distinguished Paper Award at FM 2024.

• August 2024. I will attend IJCAI 2024 in Jeju, South Korea, FM 2024 in Milan, Italy, and OOPSLA 2024 in Pasadena, CA, US. If you will be at either of these events and would like to connect, please reach out.

• July 2024. Had a wonderful time attending and meeting students at the 20th International Summer School on Trustworthy Software, at ECNU in Shanghai, China. At the summer school, together with Tom Henzinger, we gave a lecture on Trustworthy AI through Neural Certificates, Runtime Monitoring, and Multi-Agent Reasoning.

• June 2024. Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs accepted at FM 2024.

• April 2024. Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains accepted at PODC 2024. Result of an exciting collaboration with cryptography researchers, in which we used probabilistic model checking to analyze and develop novel selfish mining attacks on efficient proof system blockchains.

• April 2024. Two papers accepted at IJCAI 2024:
  • Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
  • Solving Long-run Average Reward Robust MDPs via Stochastic Games
• March 2024. Equivalence and Similarity Refutation for Probabilistic Programs accepted at PLDI 2024.