| 2024 | ATVA | Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures. | Nikola Benes, Lubos Brim, Ondrej Huvar, Samuel Pastva, David Safrnek |
| 2021 | CAV | Computing Bottom SCCs Symbolically Using Transition Guided Reduction. | Nikola Benes, Lubos Brim, Samuel Pastva, David Safrnek |
| 2021 | TACAS | Symbolic Coloured SCC Decomposition. | Nikola Benes, Lubos Brim, Samuel Pastva, David Safrnek |
| 2020 | CAV | AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks. | Nikola Benes, Lubos Brim, Jakub Kadlecaj, Samuel Pastva, David Safrnek |
| 2019 | ICFEM | Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks. | Nikola Benes, Lubos Brim, Samuel Pastva, Jakub Polcek, David Safrnek |
| 2019 | IFM | Accelerating Parameter Synthesis Using Semi-algebraic Constraints. | Nikola Benes, Lubos Brim, Martin Geletka, Samuel Pastva, David Safrnek |
| 2019 | TACAS | Digital Bifurcation Analysis of TCP Dynamics. | Nikola Benes, Lubos Brim, Samuel Pastva, David Safrnek |
| 2017 | CAV | Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems. | Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safrnek |
| 2016 | ATVA | Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems. | Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safrnek |
| 2016 | FM | A Model Checking Approach to Discrete Bifurcation Analysis. | Nikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safrnek |
| 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 | DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. | Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlcek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimr Still, Jir Weiser |
| 2013 | CAV | Exploring Parameter Space of Stochastic Biochemical Systems Using Quantitative Model Checking. | Lubos Brim, Milan Ceska, Sven Drazan, David Safrnek |
| 2012 | FMICS | Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. | Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, Petr Rockai |
| 2012 | SEFM | Checking Sanity of Software Requirements. | Jiri Barnat, Petr Bauch, Lubos Brim |
| 2012 | TASE | Executing Model Checking Counterexamples in Simulink. | Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, Italo R. Oliveira |
| 2010 | ICPADS | Employing Multiple CUDA Devices to Accelerate LTL Model Checking. | Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska |
| 2010 | SEFM | Parallel Partial Order Reduction with Topological Sort Proviso. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2009 | ICFEM | A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2009 | ICPADS | CUDA Accelerated LTL Model Checking. | Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr |
| 2009 | IFM | Partial Order Reduction for State/Event LTL. | Nikola Benes, Lubos Brim, Ivana Cern, Jiri Sochor, Pavlna Varekov, Barbora Zimmerov |
| 2008 | ATVA | DiVinE Multi-Core - A Parallel LTL Model-Checker. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2008 | FMICS | Local Quantitative LTL Model Checking. | Jiri Barnat, Lubos Brim, Ivana Cern, Milan Ceska, Jana Tumova |
| 2008 | FMICS | Can Flash Memory Help in Model Checking? | Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek |
| 2008 | ISoLA | Squeeze All the Power Out of Your Hardware to Verify Your Software!. | Jiri Barnat, Lubos Brim |
| 2008 | TACAS | Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. | Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber |
| 2007 | CAV | I/O Efficient Accepting Cycle Detection. | Jiri Barnat, Lubos Brim, Pavel Simecek |
| 2007 | ICECCS | Parallel Model Checking and the FMICS-jETI Platform. | Jiri Barnat, Lubos Brim, Martin Leucker |
| 2007 | SOFSEM | Model-Checking Large Finite-State Systems and Beyond. | Lubos Brim, Mojmr Kretnsk |
| 2006 | CAV | DiVinE - A Tool for Distributed Verification. | Jiri Barnat, Lubos Brim, Ivana Cern, Pavel Moravec, Petr Rockai, Pavel Simecek |
| 2006 | FMICS | Distributed Verification: Exploring the Power of Raw Computing Power. | Lubos Brim |
| 2006 | FMICS | On Combining Partial Order Reduction with Fairness Assumptions. | Lubos Brim, Ivana Cern, Pavel Moravec, Jir Simsa |
| 2005 | FMICS | Enhancing random walk state space exploration. | Radek Pelnek, Toms Hanzl, Ivana Cern, Lubos Brim |
| 2004 | FMCAD | Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. | Lubos Brim, Ivana Cern, Pavel Moravec, Jir Simsa |
| 2001 | SOFSEM | How to Employ Reverse Search in Distributed Single Source Shortest Paths. | Lubos Brim, Ivana Cern, Pavel Krcl, Radek Pelnek |
| 2001 | SOFSEM | Multi-agent Systems as Concurrent Constraint Processes. | Lubos Brim, David R. Gilbert, Jean-Marie Jacquet, Mojmr Kretnsk |