31 Publications

Mark all

[31]
2025 | Published | Conference Paper | IST-REx-ID: 19667 | OA
Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D. 2025. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 11158–11166.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[30]
2025 | Published | Conference Paper | IST-REx-ID: 19668 | OA
Yu E, Zikelic D, Henzinger TA. 2025. Neural control and certificate repair via runtime monitoring. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26409–26417.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[29]
2024 | Published | Conference Paper | IST-REx-ID: 18159 | OA
Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 3–12.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[28]
2024 | Published | Conference Paper | IST-REx-ID: 18160 | OA
Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[27]
2024 | Published | Conference Paper | IST-REx-ID: 17328 | OA
Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. 2024. Fully automated selfish mining analysis in efficient proof systems blockchains. Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed Computing, 268–278.
[Published Version] View | Files available | DOI | arXiv
 
[26]
2024 | Published | Journal Article | IST-REx-ID: 17162 | OA
Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2024. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 8(OOPSLA1), 107.
[Published Version] View | Files available | DOI
 
[25]
2024 | Published | Journal Article | IST-REx-ID: 17283 | OA
Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 8, 232.
[Published Version] View | Files available | DOI | arXiv
 
[24]
2024 | Published | Conference Paper | IST-REx-ID: 18155 | OA
Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods, LNCS, vol. 14933, 600–619.
[Published Version] View | Files available | DOI | arXiv
 
[23]
2023 | Published | Conference Paper | IST-REx-ID: 15023 | OA
Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, NeurIPS, .
[Published Version] View | Files available | arXiv
 
[22]
2023 | Published | Conference Paper | IST-REx-ID: 13142 | OA
Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.
[Published Version] View | Files available | DOI
 
[21]
2023 | Published | Journal Article | IST-REx-ID: 14778 | OA
Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 35(2), 11.
[Published Version] View | Files available | DOI | arXiv
 
[20]
2023 | Published | Conference Paper | IST-REx-ID: 14242 | OA
Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 14964–14973.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[19]
2023 | Published | Conference Paper | IST-REx-ID: 14559 | OA
Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning provably stabilizing neural controllers for discrete-time stochastic systems. 21st International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[18]
2023 | Published | Conference Paper | IST-REx-ID: 14518 | OA
Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications. ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.
[Published Version] View | Files available | DOI | arXiv
 
[17]
2023 | Published | Conference Paper | IST-REx-ID: 14317 | OA
Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 86–112.
[Published Version] View | Files available | DOI
 
[16]
2023 | Published | Conference Paper | IST-REx-ID: 14243 | OA
Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471.
[Published Version] View | DOI | Download Published Version (ext.) | arXiv
 
[15]
2023 | Published | Conference Paper | IST-REx-ID: 14830
Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.
[Preprint] View | Files available | DOI | arXiv
 
[14]
2023 | Published | Thesis | IST-REx-ID: 14539 | OA
Zikelic, Dorde, Automated verification and control of infinite state stochastic systems. 2023
[Published Version] View | Files available | DOI
 
[13]
2022 | Published | Conference Paper | IST-REx-ID: 11459 | OA
Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 442–457.
[Published Version] View | Files available | DOI | WoS | arXiv
 
[12]
2022 | Published | Conference Paper | IST-REx-ID: 12102 | OA
Ahmadi, Ali, Algorithms and hardness results for computing cores of Markov chains. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 250. 2022
[Published Version] View | Files available | DOI
 
[11]
2022 | Published | Conference Paper | IST-REx-ID: 12000 | OA
Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete certificates for auantitative termination analysis of probabilistic programs. Proceedings of the 34th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.
[Published Version] View | Files available | DOI | WoS
 
[10]
2022 | Published | Journal Article | IST-REx-ID: 12511 | OA
Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification in stochastic control systems via neural network supermartingales. Proceedings of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[9]
2022 | Draft | Preprint | IST-REx-ID: 14600 | OA
Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. arXiv, 2210.05308.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[8]
2022 | Draft | Preprint | IST-REx-ID: 14601 | OA
Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. arXiv, 2205.11991.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[7]
2022 | Published | Journal Article | IST-REx-ID: 12257 | OA
Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. 2022. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 106(3), 034321.
[Preprint] View | DOI | Download Preprint (ext.) | WoS | arXiv
 
[6]
2021 | Research Data Reference | IST-REx-ID: 15284 | OA
Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. RevTerm, Association for Computing Machinery, 10.1145/3410304.
[Published Version] View | Files available | DOI | Download Published Version (ext.)
 
[5]
2021 | Published | Conference Paper | IST-REx-ID: 10414 | OA
Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | WoS | arXiv
 
[4]
2021 | Published | Conference Paper | IST-REx-ID: 9644 | OA
Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1033–1048.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | WoS | arXiv
 
[3]
2021 | Published | Conference Paper | IST-REx-ID: 10665 | OA
Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized neural networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 3787–3795.
[Published Version] View | Files available | Download Published Version (ext.) | arXiv
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 10694 | OA
Avni G, Jecker IR, Zikelic D. 2021. Infinite-duration all-pay bidding games. Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 617–636.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[1]
2019 | Published | Conference Paper | IST-REx-ID: 6884 | OA
Avni, Guy, Bidding mechanisms in graph games. 138. 2019
[Published Version] View | Files available | DOI | arXiv
 

Search

Filter Publications

Display / Sort

Citation Style: ISTA Annual Report

Export / Embed

Grants


31 Publications

Mark all

[31]
2025 | Published | Conference Paper | IST-REx-ID: 19667 | OA
Chatterjee K, Goharshady E, Karrabi M, Motwani HJ, Seeliger M, Zikelic D. 2025. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 11158–11166.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[30]
2025 | Published | Conference Paper | IST-REx-ID: 19668 | OA
Yu E, Zikelic D, Henzinger TA. 2025. Neural control and certificate repair via runtime monitoring. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26409–26417.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[29]
2024 | Published | Conference Paper | IST-REx-ID: 18159 | OA
Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2024. Certified policy verification and synthesis for MDPs under distributional reach-avoidance properties. Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 3–12.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[28]
2024 | Published | Conference Paper | IST-REx-ID: 18160 | OA
Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[27]
2024 | Published | Conference Paper | IST-REx-ID: 17328 | OA
Chatterjee K, Ebrahimzadeh A, Karrabi M, Pietrzak KZ, Yeo MX, Zikelic D. 2024. Fully automated selfish mining analysis in efficient proof systems blockchains. Proceedings of the 43rd Annual ACM Symposium on Principles of Distributed Computing. PODC: Symposium on Principles of Distributed Computing, 268–278.
[Published Version] View | Files available | DOI | arXiv
 
[26]
2024 | Published | Journal Article | IST-REx-ID: 17162 | OA
Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2024. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 8(OOPSLA1), 107.
[Published Version] View | Files available | DOI
 
[25]
2024 | Published | Journal Article | IST-REx-ID: 17283 | OA
Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 8, 232.
[Published Version] View | Files available | DOI | arXiv
 
[24]
2024 | Published | Conference Paper | IST-REx-ID: 18155 | OA
Chatterjee K, Goharshady AK, Goharshady E, Karrabi M, Zikelic D. 2024. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). FM: Formal Methods, LNCS, vol. 14933, 600–619.
[Published Version] View | Files available | DOI | arXiv
 
[23]
2023 | Published | Conference Paper | IST-REx-ID: 15023 | OA
Zikelic D, Lechner M, Verma A, Chatterjee K, Henzinger TA. 2023. Compositional policy learning in stochastic control systems with formal guarantees. 37th Conference on Neural Information Processing Systems. NeurIPS: Neural Information Processing Systems, NeurIPS, .
[Published Version] View | Files available | arXiv
 
[22]
2023 | Published | Conference Paper | IST-REx-ID: 13142 | OA
Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13993, 3–25.
[Published Version] View | Files available | DOI
 
[21]
2023 | Published | Journal Article | IST-REx-ID: 14778 | OA
Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 35(2), 11.
[Published Version] View | Files available | DOI | arXiv
 
[20]
2023 | Published | Conference Paper | IST-REx-ID: 14242 | OA
Lechner M, Zikelic D, Chatterjee K, Henzinger TA, Rus D. 2023. Quantization-aware interval bound propagation for training certifiably robust quantized neural networks. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 14964–14973.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[19]
2023 | Published | Conference Paper | IST-REx-ID: 14559 | OA
Ansaripour M, Chatterjee K, Henzinger TA, Lechner M, Zikelic D. 2023. Learning provably stabilizing neural controllers for discrete-time stochastic systems. 21st International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 14215, 357–379.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[18]
2023 | Published | Conference Paper | IST-REx-ID: 14518 | OA
Avni G, Meggendorfer T, Sadhukhan S, Tkadlec J, Zikelic D. 2023. Reachability poorman discrete-bidding games. Frontiers in Artificial Intelligence and Applications. ECAI: European Conference on Artificial Intelligence vol. 372, 141–148.
[Published Version] View | Files available | DOI | arXiv
 
[17]
2023 | Published | Conference Paper | IST-REx-ID: 14317 | OA
Akshay S, Chatterjee K, Meggendorfer T, Zikelic D. 2023. MDPs as distribution transformers: Affine invariant synthesis for safety objectives. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13966, 86–112.
[Published Version] View | Files available | DOI
 
[16]
2023 | Published | Conference Paper | IST-REx-ID: 14243 | OA
Avni G, Jecker IR, Zikelic D. 2023. Bidding graph games with partially-observable budgets. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 5464–5471.
[Published Version] View | DOI | Download Published Version (ext.) | arXiv
 
[15]
2023 | Published | Conference Paper | IST-REx-ID: 14830
Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.
[Preprint] View | Files available | DOI | arXiv
 
[14]
2023 | Published | Thesis | IST-REx-ID: 14539 | OA
Zikelic, Dorde, Automated verification and control of infinite state stochastic systems. 2023
[Published Version] View | Files available | DOI
 
[13]
2022 | Published | Conference Paper | IST-REx-ID: 11459 | OA
Zikelic D, Chang B-YE, Bolignano P, Raimondi F. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 442–457.
[Published Version] View | Files available | DOI | WoS | arXiv
 
[12]
2022 | Published | Conference Paper | IST-REx-ID: 12102 | OA
Ahmadi, Ali, Algorithms and hardness results for computing cores of Markov chains. 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 250. 2022
[Published Version] View | Files available | DOI
 
[11]
2022 | Published | Conference Paper | IST-REx-ID: 12000 | OA
Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete certificates for auantitative termination analysis of probabilistic programs. Proceedings of the 34th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.
[Published Version] View | Files available | DOI | WoS
 
[10]
2022 | Published | Journal Article | IST-REx-ID: 12511 | OA
Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification in stochastic control systems via neural network supermartingales. Proceedings of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[9]
2022 | Draft | Preprint | IST-REx-ID: 14600 | OA
Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. arXiv, 2210.05308.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[8]
2022 | Draft | Preprint | IST-REx-ID: 14601 | OA
Zikelic D, Lechner M, Chatterjee K, Henzinger TA. Learning stabilizing policies in stochastic control systems. arXiv, 2205.11991.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[7]
2022 | Published | Journal Article | IST-REx-ID: 12257 | OA
Chatterjee K, Svoboda J, Zikelic D, Pavlogiannis A, Tkadlec J. 2022. Social balance on networks: Local minima and best-edge dynamics. Physical Review E. 106(3), 034321.
[Preprint] View | DOI | Download Preprint (ext.) | WoS | arXiv
 
[6]
2021 | Research Data Reference | IST-REx-ID: 15284 | OA
Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. RevTerm, Association for Computing Machinery, 10.1145/3410304.
[Published Version] View | Files available | DOI | Download Published Version (ext.)
 
[5]
2021 | Published | Conference Paper | IST-REx-ID: 10414 | OA
Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | WoS | arXiv
 
[4]
2021 | Published | Conference Paper | IST-REx-ID: 9644 | OA
Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1033–1048.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | WoS | arXiv
 
[3]
2021 | Published | Conference Paper | IST-REx-ID: 10665 | OA
Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized neural networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 3787–3795.
[Published Version] View | Files available | Download Published Version (ext.) | arXiv
 
[2]
2021 | Published | Conference Paper | IST-REx-ID: 10694 | OA
Avni G, Jecker IR, Zikelic D. 2021. Infinite-duration all-pay bidding games. Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms. SODA: Symposium on Discrete Algorithms, 617–636.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[1]
2019 | Published | Conference Paper | IST-REx-ID: 6884 | OA
Avni, Guy, Bidding mechanisms in graph games. 138. 2019
[Published Version] View | Files available | DOI | arXiv
 

Search

Filter Publications

Display / Sort

Citation Style: ISTA Annual Report

Export / Embed