| 2026 | AAAI | Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking. | Linus Heck, Filip Mack, Milan Ceska, Sebastian Junges |
| 2026 | CAV | Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families. | Milan Ceska, Sebastian Junges, Luko van der Maas, Filip Mack, Tim Quatmann |
| 2026 | CAV | Shields to Guarantee Probabilistic Safety in MDPs. | Linus Heck, Filip Mack, Roman Andriushchenko, Milan Ceska, Sebastian Junges |
| 2025 | CAV | Small Decision Trees for MDPs with Deductive Synthesis. | Roman Andriushchenko, Milan Ceska, Sebastian Junges, Filip Mack |
| 2025 | IJCAI | Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs. | Maris F. L. Galesloot, Roman Andriushchenko, Milan Ceska, Sebastian Junges, Nils Jansen |
| 2025 | UAI | Symbiotic Local Search for Small Decision Tree Policies in MDPs. | Roman Andriushchenko, Milan Ceska, Debraj Chakraborty, Sebastian Junges, Jan Kretnsk, Filip Mack |
| 2024 | ATVA | Policies Grow on Trees: Model Checking Families of MDPs. | Roman Andriushchenko, Milan Ceska, Sebastian Junges, Filip Mack |
| 2023 | CAV | Search and Explore: Symbiotic Policy Synthesis in POMDPs. | Roman Andriushchenko, Alexander Bork, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen, Filip Mack |
| 2022 | DSD | Designing Approximate Arithmetic Circuits with Combined Error Constraints. | Milan Ceska, Jir Matys, Vojtech Mrazek, Toms Vojnar |
| 2022 | UAI | Inductive synthesis of finite-state controllers for POMDPs. | Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen |
| 2021 | CAV | PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. | Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen, Simon Stupinsk |
| 2021 | TACAS | Inductive Synthesis for Probabilistic Programs Reaches New Horizons. | Roman Andriushchenko, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen |
| 2020 | CAV | SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. | Milan Ceska, Calvin Chau, Jan Kretnsk |
| 2020 | SAT | Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits. | Milan Ceska, Jir Matys, Vojtech Mrazek, Toms Vojnar |
| 2019 | CAV | Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks. | Milan Ceska, Jan Kretnsk |
| 2019 | FCCM | Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. | Milan Ceska, Vojtech Havlena, Luks Holk, Jan Korenek, Ondrej Lengl, Denis Matousek, Jir Matousek, Jakub Semric, Toms Vojnar |
| 2019 | FM | Counterexample-Driven Synthesis for Probabilistic Program Sketches. | Milan Ceska, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen |
| 2019 | TACAS | Shepherding Hordes of Markov Chains. | Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen |
| 2018 | CAV | ADAC: Automated Design of Approximate Circuits. | Milan Ceska, Jir Matys, Vojtech Mrazek, Luks Sekanina, Zdenek Vascek, Toms Vojnar |
| 2018 | TACAS | Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. | Milan Ceska, Vojtech Havlena, Luks Holk, Ondrej Lengl, Toms Vojnar |
| 2017 | CAV | Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. | Luca Cardelli, Milan Ceska, Martin Frnzle, Marta Z. Kwiatkowska, Luca Laurenti, Nicola Paoletti, Max Whitby |
| 2017 | ICCAD | Approximating complex arithmetic circuits with formal error guarantees: 32-bit multipliers accomplished. | Milan Ceska, Jir Matys, Vojtech Mrazek, Luks Sekanina, Zdenek Vascek, Toms Vojnar |
| 2017 | ICSA | Designing Robust Software Systems through Parametric Markov Chain Synthesis. | Radu Calinescu, Milan Ceska, Simos Gerasimou, Marta Kwiatkowska, Nicola Paoletti |
| 2016 | ATVA | Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. | Alessandro Abate, Milan Ceska, Marta Kwiatkowska |
| 2016 | EuroPar | Parametric Multi-step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components. | Stefano Aldegheri, Jiri Barnat, Nicola Bombieri, Federico Busato, Milan Ceska |
| 2016 | TACAS | PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. | Milan Ceska, Petr Pilar, Nicola Paoletti, Lubos Brim, Marta Z. Kwiatkowska |
| 2015 | CAV | Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks. | Alessandro Abate, Lubos Brim, Milan Ceska, Marta Z. Kwiatkowska |
| 2013 | CAV | Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. | Lubos Brim, Milan Ceska, Sven Drazan, David Safrnek |
| 2010 | ICPADS | Employing Multiple CUDA Devices to Accelerate LTL Model Checking. | Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska |
| 2009 | ICPADS | CUDA Accelerated LTL Model Checking. | Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr |
| 2008 | FMICS | Local Quantitative LTL Model Checking. | Jiri Barnat, Lubos Brim, Ivana Cern, Milan Ceska, Jana Tumova |
| 1998 | SMC | Object-oriented Petri nets, their simulation, and analysis. | Milan Ceska, Vladimr Janousek, Toms Vojnar |