Publications

^∗ equal contribution, ^† authors ordered alphabetically

Conference and Journal Papers

2025

1. Supermartingale Certificates for Quantitative Omega-regular Verification and Control
   37th International Conference on Computer Aided Verification. CAV 2025
   Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, Đorđe Žikelić^†
   coming soon

2. NeuralStoc: A Tool for Neural Stochastic Control and Verification
   37th International Conference on Computer Aided Verification. CAV 2025
   Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, Abhinav Verma, Đorđe Žikelić^†
   coming soon

3. Predictive Monitoring of Black-Box Dynamical Systems
   7th Annual Learning for Dynamics & Control Conference. L4DC 2025
   Thomas A. Henzinger, Fabian Kresse, Kaushik Mallik, Emily Yu, Đorđe Žikelić^†
   preprint

4. Refuting Equivalence in Probabilistic Programs with Conditioning
   31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Đorđe Žikelić^†
   preprint

5. Neural Control and Certificate Repair via Runtime Monitoring
   39th AAAI Conference on Artificial Intelligence. AAAI 2025
   Emily Yu, Đorđe Žikelić, Thomas A. Henzinger
   preprint

6. Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
   39th AAAI Conference on Artificial Intelligence. AAAI 2025
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Harshit J Motwani, Maximilian Seeliger, Đorđe Žikelić^†
   preprint

2024

1. Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
   26th International Symposium on Formal Methods. FM 2024
   Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Đorđe Žikelić^†
   Distinguished Paper Award
   paper, preprint

2. Fully Automated Selfish Mining Analysis in Efficient Proof Systems Blockchains
   43rd ACM Symposium on Principles of Distributed Computing. PODC 2024
   Krishnendu Chatterjee, Amirali Ebrahim-Zadeh, Mehrdad Karrabi, Krzysztof Pietrzak, Michelle Yeo, Đorđe Žikelić^†
   paper, preprint

3. Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties
   33rd International Joint Conference on Artificial Intelligence. IJCAI 2024
   S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, Đorđe Žikelić^†
   paper, preprint

4. Solving Long-run Average Reward Robust MDPs via Stochastic Games
   33rd International Joint Conference on Artificial Intelligence. IJCAI 2024
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Petr Novotný, Đorđe Žikelić^†
   paper, preprint

5. Equivalence and Similarity Refutation for Probabilistic Programs
   46th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2024
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Đorđe Žikelić^†
   paper, preprint

6. Quantitative Bounds on Resource Usage of Probabilistic Programs
   ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA 2024
   Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Đorđe Žikelić^†
   paper, preprint

2023

1. Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees
   37th Conference on Neural Information Processing Systems. NeurIPS 2023
   Đorđe Žikelić^∗, Mathias Lechner^∗, Abhinav Verma, Krishnendu Chatterjee, Thomas A. Henzinger
   paper, preprint

2. Reachability Poorman Discrete-Bidding Games
   26th European Conference on Artificial Intelligence. ECAI 2023
   Guy Avni, Tobias Meggendorfer, Suman Sadhukhan, Josef Tkadlec, Đorđe Žikelić^†
   paper, preprint

3. Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems
   21st International Symposium on Automated Technology for Verification and Analysis. ATVA 2023
   Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, Đorđe Žikelić^†
   paper, preprint

4. MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
   35th International Conference on Computer Aided Verification. CAV 2023
   S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, Đorđe Žikelić^†
   paper, preprint

5. A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems
   29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023
   Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, Đorđe Žikelić^†
   paper

6. On Lexicographic Proof Rules for Probabilistic Termination
   Formal Aspects of Computing. FAC 2023
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, Đorđe Žikelić^†
   paper

7. Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees
   37th AAAI Conference on Artificial Intelligence. AAAI 2023
   Đorđe Žikelić^∗, Mathias Lechner^∗, Krishnendu Chatterjee, Thomas A. Henzinger
   paper, preprint

8. Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks
   37th AAAI Conference on Artificial Intelligence. AAAI 2023
   Mathias Lechner, Đorđe Žikelić, Krishnendu Chatterjee, Thomas A. Henzinger, Daniela Rus
   paper, preprint

9. Bidding Graph Games with Partially-Observable Budgets
   37th AAAI Conference on Artificial Intelligence. AAAI 2023
   Guy Avni, Ismaël Jecker, Đorđe Žikelić^†
   paper, preprint

2022

1. Algorithms and Hardness Results for Computing Cores of Markov Chains
   42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2022
   Ali Ahmadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Roodabeh Safavi, Đorđe Žikelić^†
   paper, preprint

2. Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
   34th International Conference on Computer Aided Verification. CAV 2022
   Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Đorđe Žikelić^†
   paper, preprint

3. Social Balance on Networks: Local Minima and Best-edge Dynamics
   Physical Review E. PRE 2022
   Krishnendu Chatterjee, Jakub Svoboda, Đorđe Žikelić, Andreas Pavlogiannis and Josef Tkadlec
   paper, preprint

4. Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
   44th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2022
   Đorđe Žikelić, Bor-Yuh Evan Chang, Pauline Bolignano, Franco Raimondi
   Featured in the Amazon Science blog
   paper, preprint

5. Stability Verification in Stochastic Control Systems via Neural Network Supermartingales
   36th AAAI Conference on Artificial Intelligence. AAAI 2022
   Mathias Lechner^∗, Đorđe Žikelić^∗, Krishnendu Chatterjee, Thomas A. Henzinger
   paper, preprint

2021

1. Infinite Time Horizon Safety of Bayesian Neural Networks
   35th Conference on Neural Information Processing Systems. NeurIPS 2021
   Mathias Lechner^∗, Đorđe Žikelić^∗, Krishnendu Chatterjee, Thomas A. Henzinger
   paper, preprint

2. On Lexicographic Proof Rules for Probabilistic Termination
   24th International Symposium on Formal Methods. FM 2021
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, Đorđe Žikelić^†
   Invited to the Special Collection from FM 2021 dedicated to best papers
   paper, preprint

3. Proving Non-termination by Program Reversal
   43rd ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2021
   Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Đorđe Žikelić^†
   paper, preprint

4. Scalable Verification of Quantized Neural Networks
   35th AAAI Conference on Artificial Intelligence. AAAI 2021
   Thomas A. Henzinger, Mathias Lechner, Đorđe Žikelić^†
   paper, preprint

5. Bidding Mechanisms in Graph Games
   Journal of Computer and System Sciences 119. JCSS 2021
   Guy Avni, Thomas A. Henzinger, Đorđe Žikelić^†
   paper

6. Infinite-Duration All-Pay Bidding Games
   ACM-SIAM Symposium on Discrete Algorithms. SODA 2021
   Guy Avni, Ismaël Jecker, Đorđe Žikelić^†
   paper, preprint

2019

1. Bidding Mechanisms in Graph Games
   44th International Symposium on Mathematical Foundations of Computer Science. MFCS 2019
   Guy Avni, Thomas A. Henzinger, Đorđe Žikelić^†
   paper, preprint

2017

1. Optimizing Expectation with Guarantees in POMDPs
   31st AAAI Conference on Artificial Intelligence. AAAI 2017
   Krishnendu Chatterjee, Petr Novotný, Guillermo A. Perez, Jean-Francois Raskin, Đorđe Žikelić^†
   paper, preprint

2. Stochastic invariants for probabilistic termination
   44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017
   Krishnendu Chatterjee, Petr Novotný, Đorđe Žikelić^†
   paper, preprint

2014

1. Theorems about quadrilaterals and conics
   International Journal of Computer Mathematics 91 (7). Int. J. Comp. Math. 2014
   Đorđe Baralić, Branko Grbić, Đorđe Žikelić^†
   paper

Workshop Papers

2022

1. Learning Stabilizing Policies in Stochastic Control Systems
   ICLR 2022 Workshop on Socially Responsible Machine Learning (SRML). SRML@ICLR 2022
   Đorđe Žikelić^∗, Mathias Lechner^∗, Krishnendu Chatterjee, Thomas A. Henzinger
   preprint

PhD Thesis

Automated Verification and Control of Infinite State Stochastic Systems
Institute of Science and Technology Austria (ISTA). 2023
Đorđe Žikelić
thesis