Modal Logics in Timed Process Algebras. - Lubos Brim (NAPAW, 1992)

Synchronisation in Scc. - Lubos Brim; David R. Gilbert; Jean-Marie Jacquet; Mojmír Kretínský (ILPS, 1995)

A Process Algebra for Synchronous Concurrent Constraint Programming. - Lubos Brim; Jean-Marie Jacquet; David R. Gilbert; Mojmír Kretínský (ALP, 1996)

Distributed LTL Model Checking Based on Negative Cycle Detection. - Lubos Brim; Ivana Cerná; Pavel Krcál; Radek Pelánek (FSTTCS, 2001)

Randomization Helps in LTL Model Checking. - Lubos Brim; Ivana Cerná; Martin Necesal (PAPM-PROBMIV, 2001)

How to Employ Reverse Search in Distributed Single Source Shortest Paths. - Lubos Brim; Ivana Cerná; Pavel Krcál; Radek Pelánek (SOFSEM, 2001)

Multi-agent Systems as Concurrent Constraint Processes. - Lubos Brim; David R. Gilbert; Jean-Marie Jacquet; Mojmír Kretínský (SOFSEM, 2001)

Distributed LTL Model-Checking in SPIN. - Jiri Barnat; Lubos Brim; Jitka Stríbrná (SPIN, 2001)

Modelling Multi-Agent Systems as Synchronous Concurrent Constraint Processes. - Lubos Brim; Mojmír Kretínský; Jean-Marie Jacquet; David R. Gilbert (Comput. Artif. Intell., 2002)

Using Assumptions to Distribute CTL Model Checking. - Lubos Brim; Jitka Crhová; Karen Yorav (PDMC@CONCUR, 2002)

Preface. - Lubos Brim; Orna Grumberg (PDMC@CONCUR, 2002)

Coordination by Means of Synchronous and Asynchronous Communication in Concurrent Constraint Programming. - Jean-Marie Jacquet; Lubos Brim; David R. Gilbert; Mojmír Kretínský (FOCLASA, 2002)

Parallel Breadth-First Search LTL Model-Checking. - Jiri Barnat; Lubos Brim; Jakub Chaloupka (ASE, 2003)

Distributed Negative Cycle Detection Algorithms. - Lubos Brim; Ivana Cerná; Lukás Hejtmánek (PARCO, 2003)

Distribution of Explicit-State LTL Model-Checking. - Lubos Brim; Jiri Barnat (FMICS, 2003)

Using Assumptions to Distribute Alternation Free Mu-Calculus Model Checking. - Lubos Brim; Jitka Zidkova (PDMC@CAV, 2003)

Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. - Lubos Brim; Ivana Cerná; Pavel Moravec 002; Jirí Simsa (FMCAD, 2004)

From Distributed Memory Cycle Detection to Parallel LTL Model Checking. - Jiri Barnat; Lubos Brim; Jakub Chaloupka (FMICS, 2004)

Distributed Partial Order Reduction of State Spaces. - Lubos Brim; Ivana Cerná; Pavel Moravec 002; Jirí Simsa (PDMC, 2004)

Preface. - Lubos Brim; Martin Leucker (PDMC, 2004)

Cluster-Based LTL Model Checking of Large Systems. - Jiri Barnat; Lubos Brim; Ivana Cerná (FMCO, 2005)

Enhancing random walk state space exploration. - Radek Pelánek; Tomás Hanzl; Ivana Cerná; Lubos Brim (FMICS, 2005)

How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. - Lubos Brim; Ivana Cerná; Pavel Moravec 002; Jirí Simsa (PDMC@ICALP, 2005)

Preface. - Lubos Brim; Isabelle Linden (MTCoord@COORDINATION, 2005)

Introductory paper. - Lubos Brim; Orna Grumberg (Int. J. Softw. Tools Technol. Transf., 2005)

Assumption-based distribution of CTL model checking. - Lubos Brim; Karen Yorav; Jitka Zidkova (Int. J. Softw. Tools Technol. Transf., 2005)

DiVinE - A Tool for Distributed Verification. - Jiri Barnat; Lubos Brim; Ivana Cerná; Pavel Moravec 002; Petr Rockai; Pavel Simecek (CAV, 2006)

Distributed Verification: Exploring the Power of Raw Computing Power. - Lubos Brim (FMICS/PDMC, 2006)

On Combining Partial Order Reduction with Fairness Assumptions. - Lubos Brim; Ivana Cerná; Pavel Moravec 002; Jirí Simsa (FMICS/PDMC, 2006)

Foreword. - Lubos Brim; Martin Leucker (Formal Methods Syst. Des., 2006)

Component-interaction automata as a verification-oriented component-based system specification. - Lubos Brim; Ivana Cerná; Pavlína Vareková; Barbora Zimmerová (ACM SIGSOFT Softw. Eng. Notes, 2006)

I/O Efficient Accepting Cycle Detection. - Jiri Barnat; Lubos Brim; Pavel Simecek (CAV, 2007)

Component-Interaction Automata Approach (CoIn). - Barbora Zimmerová; Pavlína Vareková; Nikola Benes; Ivana Cerná; Lubos Brim; Jiri Sochor (CoCoME, 2007)

Parallel Model Checking and the FMICS-jETI Platform. - Jiri Barnat; Lubos Brim; Martin Leucker (ICECCS, 2007)

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

Model-Checking Large Finite-State Systems and Beyond. - Lubos Brim; Mojmír Kretínský (SOFSEM (1), 2007)

Scalable Multi-core LTL Model-Checking. - Jiri Barnat; Lubos Brim; Petr Rockai (SPIN, 2007)

Tutorial: Parallel Model Checking. - Lubos Brim; Jiri Barnat (SPIN, 2007)

Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. - Jiri Barnat; Lubos Brim; Ivana Cerná; Sven Drazan; David Safránek (FBTC@CONCUR, 2007)

DiVinE Multi-Core - A Parallel LTL Model-Checker. - Jiri Barnat; Lubos Brim; Petr Rockai (ATVA, 2008)

08332 Abstracts Collection - Distributed Verification and Grid Computing. - Henri E. Bal; Lubos Brim; Martin Leucker (Distributed Verification and Grid Computing, 2008)

08332 Executive Summary - Distributed Verification and Grid Computing. - Henri E. Bal; Lubos Brim; Martin Leucker (Distributed Verification and Grid Computing, 2008)

Efficient Large-Scale Model Checking. - Kees Verstoep; Henri E. Bal; Jiri Barnat; Lubos Brim (Distributed Verification and Grid Computing, 2008)

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

Can Flash Memory Help in Model Checking? - Jiri Barnat; Lubos Brim; Stefan Edelkamp; Damian Sulewski; Pavel Simecek (FMICS, 2008)

Squeeze All the Power Out of Your Hardware to Verify Your Software!. - Jiri Barnat; Lubos Brim (ISoLA, 2008)

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

Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. - Jiri Barnat; Lubos Brim; Pavel Simecek; M. Weber (TACAS, 2008)

09491 Abstracts Collection - Graph Search Engineering. - Lubos Brim; Stefan Edelkamp; Eric A. Hansen; Peter Sanders 001 (Graph Search Engineering, 2009)

A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. - Jiri Barnat; Lubos Brim; Petr Rockai (ICFEM, 2009)

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

Partial Order Reduction for State/Event LTL. - Nikola Benes; Lubos Brim; Ivana Cerná; Jiri Sochor; Pavlína Vareková; Barbora Zimmerová (IFM, 2009)

Cluster-Based I/O-Efficient LTL Model Checking. - Jiri Barnat; Lubos Brim; Pavel Simecek (ASE, 2009)

Faster Algorithm for Mean-Payoff Games. - Jakub Chaloupka; Lubos Brim (MEMICS, 2009)

BioDiVinE: A Framework for Parallel Analysis of Biological Models - Jiri Barnat; Lubos Brim; Ivana Cerná; Sven Drazan; Jana Fabriková; Jan Láník; David Safránek; Hongwu Ma (COMPMOD, 2009)

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

On algorithmic analysis of transcriptional regulation by LTL model checking. - Jiri Barnat; Lubos Brim; Ivana Cerná; Sven Drazan; Jana Fabriková; David Safránek (Theor. Comput. Sci., 2009)

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

Parallel Partial Order Reduction with Topological Sort Proviso. - Jiri Barnat; Lubos Brim; Petr Rockai (SEFM, 2010)

High-performance analysis of biological systems dynamics with the DiVinE model checker. - Jiri Barnat; Lubos Brim; David Safránek (Briefings Bioinform., 2010)

Scalable shared memory LTL model checking. - Jiri Barnat; Lubos Brim; Petr Rockai (Int. J. Softw. Tools Technol. Transf., 2010)

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

E-photosynthesis: Web-based platform for modeling of complex photosynthetic processes. - David Safránek; Jan Cervený; Matej Klement; Jana Pospísilová; Lubos Brim; Dusan Lazar; Ladislav Nedbal (Biosyst., 2011)

Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation - Lubos Brim; Jana Fabriková; Sven Drazan; David Safránek (CoRR, 2011)

Reachability in Biochemical Dynamical Systems by Quantitative Discrete Approximation (extended abstract) - Lubos Brim; Jana Fabriková; Sven Drazan; David Safránek (CompMod, 2011)

Platform Dependent Verification: On Engineering Verification Tools for 21st Century - Lubos Brim; Jiri Barnat (PDMC, 2011)

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

Faster algorithms for mean-payoff games. - Lubos Brim; Jakub Chaloupka; Laurent Doyen 001; Raffaella Gentilini; Jean-François Raskin (Formal Methods Syst. Des., 2011)

Partial order reduction for state/event LTL with application to component-interaction automata. - Nikola Benes; Lubos Brim; Barbora Buhnova; Ivana Cerná; Jiri Sochor; Pavlína Vareková (Sci. Comput. Program., 2011)

Flash memory efficient LTL model checking. - Stefan Edelkamp; Damian Sulewski; Jiri Barnat; Lubos Brim; Pavel Simecek (Sci. Comput. Program., 2011)

Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. - Jiri Barnat; Jan Beran; Lubos Brim; Tomas Kratochvila; Petr Rockai (FMICS, 2012)

Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. - Jiri Barnat; Lubos Brim; Petr Rockai (NASA Formal Methods, 2012)

Checking Sanity of Software Requirements. - Jiri Barnat; Petr Bauch; Lubos Brim (SEFM, 2012)

Executing Model Checking Counterexamples in Simulink. - Jiri Barnat; Lubos Brim; Jan Beran; Tomas Kratochvila; Italo R. Oliveira (TASE, 2012)

On Expressing and Monitoring Oscillatory Dynamics - Petr Dluhos; Lubos Brim; David Safránek (HSB, 2012)

Timed Modelling of Gene Networks with Arbitrarily Precise Expression Discretization. - S. Van Goethem; Jean-Marie Jacquet; Lubos Brim; David Safránek (CS2Bio, 2012)

Using Strategy Improvement to Stay Alive. - Lubos Brim; Jakub Chaloupka (Int. J. Found. Comput. Sci., 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)

On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. - Jiri Barnat; Lubos Brim; Petr Rockai (Sci. Comput. Program., 2012)

On Parameter Synthesis by Parallel Model Checking. - Jiri Barnat; Lubos Brim; Adam Krejci; Adam Streck; David Safránek; Martin Vejnar; Tomas Vejpustek (IEEE ACM Trans. Comput. Biol. Bioinform., 2012)

On Approximative Reachability Analysis of Biochemical Dynamical Systems. - Lubos Brim; Jana Fabriková; Sven Drazan; David Safránek (Trans. Comp. Sys. Biology, 2012)

LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. - Jiri Barnat; Lubos Brim; Vojtech Havel (ACSD, 2013)

Qualitative modelling and analysis of Photosystem II. - Lubos Brim; Vilém Ded; David Safránek (BioPPN@Petri Nets, 2013)

DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. - Jiri Barnat; Lubos Brim; Vojtech Havel; Jan Havlícek; Jan Kriho; Milan Lenco; Petr Rockai; Vladimír Still; Jirí Weiser (CAV, 2013)

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

Improved State Space Reductions for LTL Model Checking of C and C++ Programs. - Petr Rockai; Jiri Barnat; Lubos Brim (NASA Formal Methods, 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)

Robustness Analysis for Value-Freezing Signal Temporal Logic. - Lubos Brim; Tomas Vejpustek; David Safránek; Jana Fabriková (HSB, 2013)

Compact Representation of Photosynthesis Dynamics by Rule-based Models (Full Version). - Lubos Brim; Juraj Niznan; David Safránek (CoRR, 2014)

Model Checking C++ with Exceptions. - Petr Rockai; Jiri Barnat; Lubos Brim (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014)

Compact Representation of Photosynthesis Dynamics by Rule-based Models. - Lubos Brim; Juraj Niznan; David Safránek (SASB, 2014)

STL⁎: Extending signal temporal logic with signal-value freezing operator. - Lubos Brim; Petr Dluhos; David Safránek; Tomas Vejpustek (Inf. Comput., 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)

High-Performance Discrete Bifurcation Analysis for Piecewise-Affine Dynamical Systems. - Lubos Brim; Martin Demko; Samuel Pastva; David Safránek (HSB, 2015)

Analysing Sanity of Requirements for Avionics Systems (Preliminary Version). - Jiri Barnat; Petr Bauch; Nikola Benes; Lubos Brim; Jan Beran; Tomas Kratochvila (CoRR, 2015)

Formal Biochemical Space with Semantics in Kappa and BNGL. - T. Ded; David Safránek; Matej Troják; Matej Klement; Jakub Salagovic; Lubos Brim (SASB, 2015)

Parallel SMT-Based Parameter Synthesis with Application to Piecewise Multi-affine Systems. - Nikola Benes; Lubos Brim; Martin Demko; Samuel Pastva; David Safránek (ATVA, 2016)

High-Performance Symbolic Parameter Synthesis of Biological Models: A Case Study. - Martin Demko; Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (CMSB, 2016)

A Model Checking Approach to Discrete Bifurcation Analysis. - Nikola Benes; Lubos Brim; Martin Demko; Samuel Pastva; David Safránek (FM, 2016)

Toward Modelling and Analysis of Transient and Sustained Behaviour of Signalling Pathways. - Matej Hajnal; David Safránek; Martin Demko; Samuel Pastva; Pavel Krejcí; Lubos Brim (HSB, 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)

Analysing sanity of requirements for avionics systems. - Jiri Barnat; Petr Bauch; Nikola Benes; Lubos Brim; Jan Beran; Tomas Kratochvila (Formal Aspects Comput., 2016)

Model checking C++ programs with exceptions. - Petr Rockai; Jiri Barnat; Lubos Brim (Sci. Comput. Program., 2016)

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems. - Nikola Benes; Lubos Brim; Martin Demko; Samuel Pastva; David Safránek (CAV (1), 2017)

Detecting Attractors in Biological Models with Uncertain Parameters. - Jiri Barnat; Nikola Benes; Lubos Brim; Martin Demko; Matej Hajnal; Samuel Pastva; David Safránek (CMSB, 2017)

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

Barbaric Robustness Monitoring Revisited for STL* in Parasim. - David Safránek; Matej Troják; Vojtech Bruza; Tomás Vejpustek; Jan Papousek; Martin Demko; Samuel Pastva; Ales Pejznoch; Lubos Brim (CMSB, 2019)

Facetal abstraction for non-linear dynamical systems based on δ-decidable SMT. - Nikola Benes; Lubos Brim; Jana Drazanová; Samuel Pastva; David Safránek (HSCC, 2019)

Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks. - Nikola Benes; Lubos Brim; Samuel Pastva; Jakub Polácek; David Safránek (ICFEM, 2019)

Accelerating Parameter Synthesis Using Semi-algebraic Constraints. - Nikola Benes; Lubos Brim; Martin Geletka; Samuel Pastva; David Safránek (IFM, 2019)

Digital Bifurcation Analysis of TCP Dynamics. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (TACAS (2), 2019)

Model Checking Approach to the Analysis of Biological Systems. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (Automated Reasoning for Systems Biology and Medicine, 2019)

AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks. - Nikola Benes; Lubos Brim; Jakub Kadlecaj; Samuel Pastva; David Safránek (CAV (1), 2020)

Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications. - Eva Smijáková; Samuel Pastva; David Safránek; Lubos Brim (CMSB, 2020)

eBCSgen: A Software Tool for Biochemical Space Language. - Matej Troják; David Safránek; Lukrécia Mertová; Lubos Brim (CMSB, 2020)

Parameter Synthesis and Robustness Analysis of Rule-Based Models. - Matej Troják; David Safránek; Lukrécia Mertová; Lubos Brim (NFM, 2020)

Executable Biochemical Space for Specification and Analysis of Biochemical Systems. - Matej Troják; David Safránek; Lubos Brim; Jakub Salagovic; Jan Cervený (SASB, 2020)

Executable Biochemical Space for Specification and Analysis of Biochemical Systems. - Matej Troják; David Safránek; Lubos Brim (CoRR, 2020)

Parallel One-Step Control of Parametrised Boolean Networks. - Lubos Brim; Samuel Pastva; David Safránek; Eva Smijakova (CoRR, 2020)

Digital Bifurcation Analysis of Internet Congestion Control Protocols. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (Int. J. Bifurc. Chaos, 2020)

Parallel parameter synthesis algorithm for hybrid CTL. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (Sci. Comput. Program., 2020)

Computing Bottom SCCs Symbolically Using Transition Guided Reduction. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (CAV (1), 2021)

Aeon 2021: Bifurcation Decision Trees in Boolean Networks. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (CMSB, 2021)

Symbolic Coloured SCC Decomposition. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (TACAS (2), 2021)

Regulated Multiset Rewriting Systems. - Matej Troják; Samuel Pastva; David Safránek; Lubos Brim (CoRR, 2021)

eBCSgen 2.0: Modelling and Analysis of Regulated Rule-Based Systems. - Matej Troják; David Safránek; Branislav Brozmann; Lubos Brim (CMSB, 2022)

Exploring attractor bifurcations in Boolean networks. - Nikola Benes; Lubos Brim; Jakub Kadlecaj; Samuel Pastva; David Safránek (BMC Bioinform., 2022)

Biochemical Space Language in Relation to Multiset Rewriting Systems. - Matej Troják; David Safránek; Lubos Brim (CoRR, 2022)

Robust Control of Partially Specified Boolean Networks. - Lubos Brim; Samuel Pastva; David Safránek; Eva Smijáková (CoRR, 2022)

BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek (Log. Methods Comput. Sci., 2022)

AEON.py: Python library for attractor analysis in asynchronous Boolean networks. - Nikola Benes; Lubos Brim; Ondrej Huvar; Samuel Pastva; David Safránek; Eva Smijáková (Bioinform., 2022)

Phenotype Control of Partially Specified Boolean Networks. - Nikola Benes; Lubos Brim; Samuel Pastva; David Safránek; Eva Smijáková (CMSB, 2023)

Temporary and permanent control of partially specified Boolean networks. - Lubos Brim; Samuel Pastva; David Safránek; Eva Smijáková (Biosyst., 2023)

Rule-based modelling of biological systems using regulated rewriting. - Matej Troják; David Safránek; Samuel Pastva; Lubos Brim (Biosyst., 2023)

Boolean network sketches: a unifying framework for logical model inference. - Nikola Benes; Lubos Brim; Ondrej Huvar; Samuel Pastva; David Safránek (Bioinform., 2023)

Symbolic Model Checking of Hybrid CTL on Coloured Kripke Structures. - Nikola Benes; Lubos Brim; Ondrej Huvar; Samuel Pastva; David Safránek (ATVA (2), 2024)

BNClassifier: Classifying Boolean Models by Dynamic Properties. - Nikola Benes; Lubos Brim; Ondrej Huvar; Samuel Pastva; David Safránek (CMSB, 2024)