ProbDiVinE: A Parallel Qualitative LTL Model Checker. - Jiri Barnat; Lubos Brim; Ivana Cerná; Milan Ceska 002; Jana Tumova (QEST, 2007)

Local Quantitative LTL Model Checking. - Jiri Barnat; Lubos Brim; Ivana Cerná; Milan Ceska 002; Jana Tumova (FMICS, 2008)

ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. - Jiri Barnat; Lubos Brim; Ivana Cerná; Milan Ceska 002; Jana Tumova (QEST, 2008)

Preface. - Milan Ceska 002; Zdenek Kotásek; Mojmír Kretínský; Ludek Matyska; Tomás Vojnar (MEMICS, 2008)

CUDA Accelerated LTL Model Checking. - Jiri Barnat; Lubos Brim; Milan Ceska 002; Tomas Lamr (ICPADS, 2009)

DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking - Jiri Barnat; Lubos Brim; Milan Ceska 002 (PDMC, 2009)

Employing Multiple CUDA Devices to Accelerate LTL Model Checking. - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (ICPADS, 2010)

CUDA Accelerated LTL Model Checking - Revisited. - Petr Bauch; Milan Ceska 002 (MEMICS, 2010)

Computing Strongly Connected Components in Parallel on CUDA. - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (IPDPS, 2011)

Computing Optimal Cycle Mean in Parallel on CUDA - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (PDMC, 2011)

On Parallel Software Verification Using Boolean Equation Systems. - Alexander Ditter; Milan Ceska 002; Gerald Lüttgen (SPIN, 2012)

Designing fast LTL model checking algorithms for many-core GPUs. - Jiri Barnat; Petr Bauch; Lubos Brim; Milan Ceska 002 (J. Parallel Distributed Comput., 2012)

Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. - Lubos Brim; Milan Ceska 002; Sven Drazan; David Safránek (CAV, 2013)

Model Checking of Biological Systems. - Lubos Brim; Milan Ceska 002; David Safránek (SFM, 2013)

On Robustness Analysis of Stochastic Biochemical Systems by Probabilistic Model Checking. - Lubos Brim; Milan Ceska 002; Sven Drazan; David Safránek (CoRR, 2013)

Precise Parameter Synthesis for Stochastic Biochemical Systems. - Milan Ceska 002; Frits Dannenberg; Marta Z. Kwiatkowska; Nicola Paoletti (CMSB, 2014)

Adaptive Aggregation of Markov Chains: Quantitative Analysis of Chemical Reaction Networks. - Alessandro Abate; Lubos Brim; Milan Ceska 002; Marta Z. Kwiatkowska (CAV (1), 2015)

Parameter Synthesis by Parallel Coloured CTL Model Checking. - Lubos Brim; Milan Ceska 002; Martin Demko; Samuel Pastva; David Safránek (CMSB, 2015)

Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. - Alessandro Abate; Milan Ceska 002; Marta Kwiatkowska (ATVA, 2016)

Parametric Multi-step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components. - Stefano Aldegheri; Jiri Barnat; Nicola Bombieri; Federico Busato; Milan Ceska 002 (Euro-Par Workshops, 2016)

PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. - Milan Ceska 002; Petr Pilar; Nicola Paoletti; Lubos Brim; Marta Z. Kwiatkowska (TACAS, 2016)

Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. - Luca Cardelli; Milan Ceska 002; Martin Fränzle; Marta Z. Kwiatkowska; Luca Laurenti; Nicola Paoletti; Max Whitby (CAV (2), 2017)

Precise Parameter Synthesis for Generalised Stochastic Petri Nets with Interval Parameters. - Milan Ceska Jr.; Milan Ceska 001; Nicola Paoletti (EUROCAST (2), 2017)

Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision. - Luca Laurenti; Alessandro Abate; Luca Bortolussi; Luca Cardelli; Milan Ceska 002; Marta Z. Kwiatkowska (HSCC, 2017)

Approximating complex arithmetic circuits with formal error guarantees: 32-bit multipliers accomplished. - Milan Ceska 002; Jirí Matyás; Vojtech Mrazek; Lukás Sekanina; Zdenek Vasícek; Tomás Vojnar (ICCAD, 2017)

Designing Robust Software Systems through Parametric Markov Chain Synthesis. - Radu Calinescu; Milan Ceska 002; Simos Gerasimou; Marta Kwiatkowska; Nicola Paoletti (ICSA, 2017)

RODES: A Robust-Design Synthesis Tool for Probabilistic Systems. - Radu Calinescu; Milan Ceska 002; Simos Gerasimou; Marta Kwiatkowska; Nicola Paoletti (QEST, 2017)

Precise parameter synthesis for stochastic biochemical systems. - Milan Ceska 002; Frits Dannenberg; Nicola Paoletti; Marta Kwiatkowska; Lubos Brim (Acta Informatica, 2017)

ADAC: Automated Design of Approximate Circuits. - Milan Ceska 002; Jirí Matyás; Vojtech Mrazek; Lukás Sekanina; Zdenek Vasícek; Tomás Vojnar (CAV (1), 2018)

Efficient synthesis of robust models for stochastic systems. - Radu Calinescu; Milan Ceska 002; Simos Gerasimou; Marta Kwiatkowska; Nicola Paoletti (J. Syst. Softw., 2018)

Erratum to "Efficient synthesis of robust models for stochastic systems" [The Journal of Systems & Software 143 (2018) 140-158]. - Radu Calinescu; Milan Ceska 002; Simos Gerasimou; Marta Kwiatkowska; Nicola Paoletti (J. Syst. Softw., 2018)

Model Repair Revamped - - On the Automated Synthesis of Markov Chains -. - Milan Ceska 002; Christian Dehnert; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (From Reactive Systems to Cyber-Physical Systems, 2019)

Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks. - Milan Ceska 002; Jan Kretínský (CAV (1), 2019)

Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract). - Milan Ceska 002; Jan Kretínský (CMSB, 2019)

Approximating Complex Arithmetic Circuits with Guaranteed Worst-Case Relative Error. - Milan Ceska Jr.; Milan Ceska 001; Jirí Matyás; Adam Pankuch; Tomás Vojnar (EUROCAST (1), 2019)

Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. - Milan Ceska 002; Vojtech Havlena; Lukás Holík; Jan Korenek; Ondrej Lengál; Denis Matousek; Jirí Matousek 002; Jakub Semric; Tomás Vojnar (FCCM, 2019)

Counterexample-Driven Synthesis for Probabilistic Program Sketches. - Milan Ceska 002; Christian Hensel; Sebastian Junges; Joost-Pieter Katoen (FM, 2019)

Shepherding Hordes of Markov Chains. - Milan Ceska 002; Nils Jansen 001; Sebastian Junges; Joost-Pieter Katoen (TACAS (2), 2019)

SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. - Milan Ceska 002; Calvin Chau; Jan Kretínský (CAV (1), 2020)

Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits. - Milan Ceska 002; Jirí Matyás; Vojtech Mrazek; Tomás Vojnar (SAT, 2020)

Adaptive verifiability-driven strategy for evolutionary approximation of arithmetic circuits. - Milan Ceska 002; Jirí Matyás; Vojtech Mrazek; Lukás Sekanina; Zdenek Vasícek; Tomás Vojnar (Appl. Soft Comput., 2020)

Approximate reduction of finite automata for high-speed network intrusion detection. - Milan Ceska 002; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Tomás Vojnar (Int. J. Softw. Tools Technol. Transf., 2020)

PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Simon Stupinský (CAV (1), 2021)

Inductive Synthesis for Probabilistic Programs Reaches New Horizons. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen (TACAS (1), 2021)

Counterexample-guided inductive synthesis for probabilistic systems. - Milan Ceska 002; Christian Hensel; Sebastian Junges; Joost-Pieter Katoen (Formal Aspects Comput., 2021)

Adaptive formal approximations of Markov chains. - Alessandro Abate; Roman Andriushchenko; Milan Ceska 002; Marta Kwiatkowska (Perform. Evaluation, 2021)

Abstraction-Based Segmental Simulation of Chemical Reaction Networks. - Martin Helfrich; Milan Ceska 002; Jan Kretínský; Stefan Marticek (CMSB, 2022)

GPU-Accelerated Synthesis of Probabilistic Programs. - Roman Andriushchenko; Milan Ceska 002; Vladimír Marcin; Tomás Vojnar (EUROCAST, 2022)

Inductive synthesis of finite-state controllers for POMDPs. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen (UAI, 2022)

Designing Approximate Arithmetic Circuits with Combined Error Constraints. - Milan Ceska 002; Jirí Matyás; Vojtech Mrazek; Tomás Vojnar (CoRR, 2022)

SagTree: Towards efficient mutation in evolutionary circuit approximation. - Milan Ceska 002; Jirí Matyás; Vojtech Mrazek; Lukás Sekanina; Zdenek Vasícek; Tomás Vojnar (Swarm Evol. Comput., 2022)

Artifact for CMSB22 paper "Abstraction-Based Segmental Simulation of Chemical Reaction Networks". - Martin Helfrich; Milan Ceska 002; Jan Kretínský; Stefan Marticek (Zenodo, 2022)

Search and Explore: Symbiotic Policy Synthesis in POMDPs. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (CAV (3), 2023)

Deductive Controller Synthesis for Probabilistic Hyperproperties. - Roman Andriushchenko; Ezio Bartocci; Milan Ceska 002; Francesco Pontiggia; Sarah Sallinger (QEST, 2023)

Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (TOOLympics@ETAPS, 2023)

Artifact supplement for 'Search and Explore: Symbiotic Policy Synthesis in POMDPs'. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2023)

Artifact supplement for 'Search and Explore: Symbiotic Policy Synthesis in POMDPs'. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2023)

Artifact supplement for 'Search and Explore: Symbiotic Policy Synthesis in POMDPs'. - Roman Andriushchenko; Alexander Bork; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2023)

Artifact supplement for "Deductive Controller Synthesis for Probabilistic Hyperproperties". - Roman Andriushchenko; Ezio Bartocci; Milan Ceska 002; Francesco Pontiggia; Sarah Sallinger (Zenodo, 2023)

Artifact supplement for "Deductive Controller Synthesis for Probabilistic Hyperproperties". - Roman Andriushchenko; Ezio Bartocci; Milan Ceska 002; Francesco Pontiggia; Sarah Sallinger (Zenodo, 2023)

Artifact supplement for "Deductive Controller Synthesis for Probabilistic Hyperproperties". - Roman Andriushchenko; Ezio Bartocci; Milan Ceska 002; Francesco Pontiggia; Sarah Sallinger (Zenodo, 2023)

Artifact supplement for "Deductive Controller Synthesis for Probabilistic Hyperproperties". - Roman Andriushchenko; Ezio Bartocci; Milan Ceska 002; Francesco Pontiggia; Sarah Sallinger (Zenodo, 2023)

Artifact supplement for "Deductive Controller Synthesis for Probabilistic Hyperproperties". - Roman Andriushchenko; Ezio Bartocci; Milan Ceska 002; Francesco Pontiggia; Sarah Sallinger (Zenodo, 2023)

Policies Grow on Trees: Model Checking Families of MDPs. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Filip Macák (ATVA (2), 2024)

Tools at the Frontiers of Quantitative Verification. - Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Ceska 002; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; Nils Jansen 001; Joshua Jeppson; Sebastian Junges; Maximilian A. Köhl; et al. (CoRR, 2024)

Artifact supplement for 'An Oracle-Guided Approach to Constrained Controller Synthesis Under Uncertainty'. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2024)

Artifact supplement for 'An Oracle-Guided Approach to Constrained Controller Synthesis Under Uncertainty'. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2024)

Artifact supplement for 'An Oracle-Guided Approach to Constrained Controller Synthesis Under Uncertainty'. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Joost-Pieter Katoen; Filip Macák (Zenodo, 2024)

Abstraction-based segmental simulation of reaction networks using adaptive memoization. - Martin Helfrich; Roman Andriushchenko; Milan Ceska 002; Jan Kretínský; Stefan Marticek; David Safránek (BMC Bioinform., 2024)

Small Decision Trees for MDPs with Deductive Synthesis. - Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Filip Macák (CAV (2), 2025)

Decentralized Planning Using Probabilistic Hyperproperties. - Francesco Pontiggia; Filip Macák; Roman Andriushchenko; Michele Chiari; Milan Ceska 002 (AAMAS, 2025)

Symbiotic Local Search for Small Decision Tree Policies in MDPs. - Roman Andriushchenko; Milan Ceska 002; Debraj Chakraborty 002; Sebastian Junges; Jan Kretínský; Filip Macák (UAI, 2025)

An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty. - Roman Andriushchenko; Milan Ceska 002; Filip Macák; Sebastian Junges; Joost-Pieter Katoen (J. Artif. Intell. Res., 2025)

rfPG: Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs. - Maris F. L. Galesloot; Roman Andriushchenko; Milan Ceska 002; Sebastian Junges; Nils Jansen 001 (CoRR, 2025)