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.

I have multiple openings for motivated PhD students, interns, and visiting PhD/master/undergrad students, to work with me on topics listed below, or more broadly on topics related to formal methods, trustworthy AI or program verification. See this page for more details.

Research Interests

My research is concerned with designing theories and automated methods for ensuring that software and AI systems are correct, safe, and trustworthy. To achieve this, I study Formal Methods and Programming Languages as well as Trustworthy AI and Safe Autonomy. My research is both foundational and application driven. On the foundational side, the long-term goal of my work is to contribute to laying theoretical and algorithmic foundations of automated formal verification and synthesis methods for probabilistic models and programs. Probabilistic models and programs provide a canonical framework for modelling and implementing computing systems that exhibit uncertain behaviour, with a broad range of applications such as randomised algorithms, communication protocols and networks, security and privacy protocols, control and autonomous systems, and AI. The central application domains that I focus on are trustworthy AI and safe autonomy, where my goal is to develop certified learning and formal verification methods for designing trustworthy AI and safe autonomous systems. My current research interests with some selected prior work include:

1. Formal Methods for Probabilistic Models and Programs
   • Probabilistic model and program verification (CAV25, IJCAI24, PLDI24, OOPSLA24, CAV23, CAV22, POPL17)
   • Non-probabilistic program verification (FM24, PLDI22, PLDI21) and efficient template-based synthesis in programs (ATVA25b, AAAI25)
2. Trustworthy AI and Safe Autonomy
   • Certified neural control and safe RL (AAAI25a, TOSEM25, NeurIPS23, AAAI23a, AAAI22)
   • Certified learning and formal verification of ML models (e.g. neural networks) (AAAI23b, NeurIPS21, AAAI21)
3. Broader perspective and other applications of probabilistic system verification:
   • Bidding games on graphs (AAAI23c, SODA21)
   • Blockchain protocol analysis (PODC24)

News

• October 2025. We will organise the second Singapore Programming Languages Summit on November 24, to be held at SMU. If you are a PL researcher based in Singapore (or will be visiting Singapore at the time), please consider participating and also presenting your work at the summit! More details here.

• October 2025. We will organise the inaugural Workshop on Post-AI Formal Methods (P-AI-FM) on January 26, co-located with AAAI 2026 in Singapore. We look forward to receiving your work and seeing you at the workshop! More details at the workshop website.

• October 2025. PolyQEnt: A Polynomial Quantified Entailment Solver has received a Distinguished Tool Paper award at ATVA 2025!

• October 2025. Synthesizing Efficient and Permissive Programmatic Runtime Shields for Neural Policies accepted at TOSEM.

• October 2025. I was awarded the Ministry of Education (MOE) Tier 1b grant for the project “Relational Verification of Probabilistic Models and Programs”. I have multiple openings for motivated PhD students and interns. Reach out if interested and see here for more details!

• July 2025. I will attend CAV 2025 in Zagreb, Croatia, and CONCUR 2025 in Aarhus, Denmark. If you will be around and would like to catch up or connect, please reach out!

• May 2025. Omega-regular Verification and Control for Distributional Specifications in MDPs accepted at CONCUR 2025. This work was completed while Ouldouz Neysari was a visiting student in my group, congrats!

• 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. This work was completed while Pouya Sadeghi was a visiting student in my group, congrats!

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