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 and the Outstanding Scientific Achievement awards at ISTA. 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 verification. Please see this page if interested.

Research Interests

My research is concerned with helping programmers ensure that software and AI systems are correct, safe, and trustworthy. To achieve this, I study Formal Methods and their applications to Program Analysis and Verification as well as Trustworthy AI and Safe Autonomy. The long-term goal of my work is to advance the theory and automation of formal methods for certifying the correctness of software and AI systems in the presence of probabilistic uncertainty, going beyond the classical finite-state probabilistic model checking paradigm. 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 software and AI systems in practice. My current research interests include:

1. Program Analysis and Verification
   • Probabilistic models and programs (CAV25, TACAS25, PLDI24, OOPSLA24, FAC23, CAV22, POPL17)
   • Numerical programs (FM24, PLDI22, PLDI21)
   • Efficient quantifier elimination for template-based synthesis in programs (AAAI25b, arXiv24)
2. Trustworthy AI and Safe Autonomy
   • Certification for learning-enabled control and safe RL (AAAI25a, NeurIPS23, ATVA23, TACAS23, AAAI23a, AAAI22, NeurIPS21)
   • Formal verification and planning in Markov models (CAV25, IJCAI24a, IJCAI24b, CAV23, FSTTCS22)
   • Formal verification of learned systems (e.g. neural networks) (AAAI23b, NeurIPS21, AAAI21)
3. Broader perspective and applications of probabilistic system verification:
   • Bidding games on graphs (ECAI23, AAAI23c, SODA21, JCSS21)
   • Blockchain protocol analysis (PODC24)

News

• May 2025. Omega-regular Verification and Control for Distributional Specifications in MDPs accepted at CONCUR 2025.

• May 2025. LP-Based Weighted Model Integration over Non-Linear Real Arithmetic accepted at IJCAI 2025.

• April 2025. Supermartingale Certificates for Quantitative Omega-regular Verification and Control accepted at CAV 2025.

• February 2025. Predictive Monitoring of Black-Box Dynamical Systems accepted at L4DC 2025.

• February 2025. I will attend AAAI 2025 in Philadelphia, PA, US. If you will around and would like to connect, please reach out.

• December 2024. Refuting Equivalence in Probabilistic Programs with Conditioning accepted at TACAS 2025.

• December 2024. Two papers accepted at AAAI 2025:
  • Neural Control and Certificate Repair via Runtime Monitoring
  • Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization

• 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.
• 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.