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

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

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

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

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

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

Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. - Jiri Barnat; Pavel Moravec 002 (FMICS/PDMC, 2006)

Distributed breadth-first search LTL model checking. - Jiri Barnat; Ivana Cerná (Formal Methods Syst. Des., 2006)

I/O Efficient Accepting Cycle Detection. - Jiri Barnat; Lubos Brim; Pavel Simecek (CAV, 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)

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)

Improved Distributed Algorithms for SCC Decomposition. - Jiri Barnat; Jakub Chaloupka; Jaco van de Pol (PDMC@CAV, 2007)

Shared Hash Tables in Parallel Model Checking. - Jiri Barnat; Petr Rockai (PDMC@CAV, 2007)

DiVinE Multi-Core - A Parallel LTL Model-Checker. - Jiri Barnat; Lubos Brim; Petr Rockai (ATVA, 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)

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)

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

Quantitative Model Checking of Systems with Degradation. - Jiri Barnat; Ivana Cerná; Jana Tumova (QEST, 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)

A symbolic approach to controlling piecewise affine systems. - Jana Tumova; Boyan Yordanov; Calin Belta; Ivana Cerna; Jiri Barnat (CDC, 2010)

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)

Timed Automata Approach to Verification of Systems with Degradation. - Jiri Barnat; Ivana Cerná; Jana Tumova (MEMICS, 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)

Distributed Algorithms for SCC Decomposition. - Jiri Barnat; Jakub Chaloupka; Jaco van de Pol (J. Log. Comput., 2011)

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

Attraction-based receding horizon path planning with temporal logic constraints. - María Svorenová; Jana Tumova; Jiri Barnat; Ivana Cerna (CDC, 2012)

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)

Verification of Systems with Degradation. - Jiri Barnat; Ivana Cerná; Jana Tumova (Comput. Informatics, 2012)

Distributed LTL Model Checking with Hash Compaction. - Jiri Barnat; Jan Havlícek; Petr Rockai (PASM/PDMC, 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)

Temporal Logic Control of Discrete-Time Piecewise Affine Systems. - Boyan Yordanov; Jana Tumova; Ivana Cerna; Jiri Barnat; Calin Belta (IEEE Trans. Autom. Control., 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)

LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. - Jiri Barnat; Lubos Brim; Vojtech Havel (ACSD, 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)

DCCL: verification of component systems with ensembles. - Jiri Barnat; Nikola Benes; Ivana Cerná; Zuzana Petruchová (CBSE, 2013)

Towards Verification of Ensemble-Based Component Systems. - Jiri Barnat; Nikola Benes; Tomás Bures; Ivana Cerná; Jaroslav Keznikl; Frantisek Plásil (FACS, 2013)

Improved State Space Reductions for LTL Model Checking of C and C++ Programs. - Petr Rockai; Jiri Barnat; Lubos Brim (NASA Formal Methods, 2013)

Formal analysis of piecewise affine systems through formula-guided refinement. - Boyan Yordanov; Jana Tumova; Ivana Cerná; Jiri Barnat; Calin Belta (Autom., 2013)

Control Explicit—Data Symbolic Model Checking: An Introduction - Jiri Barnat; Petr Bauch (CoRR, 2013)

Temporal Verification of Simulink Diagrams. - Jiri Barnat; Petr Bauch; Vojtech Havel (HASE, 2014)

On Clock-Aware LTL Properties of Timed Automata. - Peter Bezdek; Nikola Benes; Vojtech Havel; Jiri Barnat; Ivana Cerná (ICTAC, 2014)

LTL Model Checking of LLVM Bitcode with Symbolic Data. - Petr Bauch; Vojtech Havel; Jiri Barnat (MEMICS, 2014)

Context-Switch-Directed Verification in DIVINE. - Vladimír Still; Petr Rockai; Jiri Barnat (MEMICS, 2014)

Model Checking Parallel Programs with Inputs. - Jiri Barnat; Petr Bauch; Vojtech Havel (PDP, 2014)

LTL Model Checking of Parametric Timed Automata. - Peter Bezdek; Nikola Benes; Vojtech Havel; Jiri Barnat; Ivana Cerná (CoRR, 2014)

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

Weak Memory Models as LLVM-to-LLVM Transformations. - Vladimír Still; Petr Rockai; Jiri Barnat (MEMICS, 2015)

Techniques for Memory-Efficient Model Checking of C and C++ Code. - Petr Rockai; Vladimír Still; Jiri Barnat (SEFM, 2015)

Quo Vadis Explicit-State Model Checking. - Jiri Barnat (SOFSEM, 2015)

Fast, Dynamically-Sized Concurrent Hash Table. - Jiri Barnat; Petr Rockai; Vladimír Still; Jirí Weiser (SPIN, 2015)

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

Optimal observation mode scheduling for systems under temporal constraints. - Eva Tesarova; María Svorenová; Jiri Barnat; Ivana Cerna (ACC, 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)

Tunable Online MUS/MSS Enumeration. - Jaroslav Bendík; Nikola Benes; Ivana Cerná; Jiri Barnat (FSTTCS, 2016)

On verifying C++ programs with probabilities. - Jiri Barnat; Ivana Cerná; Petr Rockai; Vladimír Still; Kristína Zákopcanová (SAC, 2016)

Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. - Jaroslav Bendík; Nikola Benes; Jiri Barnat; Ivana Cerná (SEFM, 2016)

LTL Parameter Synthesis of Parametric Timed Automata. - Peter Bezdek; Nikola Benes; Jiri Barnat; Ivana Cerná (SEFM, 2016)

SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. - Jan Mrázek; Petr Bauch; Henrich Lauko; Jiri Barnat (SPIN, 2016)

DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). - Vladimír Still; Petr Rockai; Jiri Barnat (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)

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories. - Petr Bauch; Vojtech Havel; Jiri Barnat (Softw. Qual. J., 2016)

Control Explicit-Data Symbolic Model Checking. - Petr Bauch; Vojtech Havel; Jiri Barnat (ACM Trans. Softw. Eng. Methodol., 2016)

Model Checking of C and C++ with DIVINE 4. - Zuzana Baranová; Jiri Barnat; Katarína Kejstová; Tadeás Kucera; Henrich Lauko; Jan Mrázek; Petr Rockai; Vladimír Still (ATVA, 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)

Using Off-the-Shelf Exception Support Components in C++ Verification. - Vladimír Still; Petr Rockai; Jiri Barnat (QRS, 2017)

From Model Checking to Runtime Verification and Back. - Katarína Kejstová; Petr Rockai; Jiri Barnat (RV, 2017)

Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution). - Jan Mrázek; Martin Jonás; Vladimír Still; Henrich Lauko; Jiri Barnat (TACAS (2), 2017)

DiVM: Model Checking with LLVM and Graph Memory. - Petr Rockai; Ivana Cerná; Jiri Barnat (CoRR, 2017)

SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking. - Jan Mrázek; Martin Jonás; Jiri Barnat (CoRR, 2017)

Parallel Model Checking Algorithms for Linear-Time Temporal Logic. - Jiri Barnat; Vincent Bloemen; Alexandre Duret-Lutz; Alfons Laarman; Laure Petrucci; Jaco van de Pol; Etienne Renault (Handbook of Parallel Constraint Reasoning, 2018)

Model Checking of C++ Programs Under the x86-TSO Memory Model. - Vladimír Still; Jiri Barnat (ICFEM, 2018)

Symbolic Computation via Program Transformation. - Henrich Lauko; Petr Rockai; Jiri Barnat (ICTAC, 2018)

On clock-aware LTL parameter synthesis of timed automata. - Peter Bezdek; Nikola Benes; Ivana Cerná; Jiri Barnat (J. Log. Algebraic Methods Program., 2018)

DiVM: Model checking with LLVM and graph memory. - Petr Rockai; Vladimír Still; Ivana Cerná; Jiri Barnat (J. Syst. Softw., 2018)

A Simulator for LLVM Bitcode. - Petr Rockai; Jiri Barnat (FMICS, 2019)

RoFICoM - First Open-Hardware Connector for Metamorphic Robots. - Jan Mrázek; Jiri Barnat (IROS, 2019)

Local Nontermination Detection for Parallel C++ Programs. - Vladimír Still; Jiri Barnat (SEFM, 2019)

Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution). - Henrich Lauko; Vladimír Still; Petr Rockai; Jiri Barnat (TACAS (3), 2019)

On Symbolic Execution of Decompiled Programs. - Lukás Korencik; Petr Rockai; Henrich Lauko; Jiri Barnat (QRS, 2020)

Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? - Jan Mrázek; Martin Jonás; Jiri Barnat (IROS, 2021)

Reproducible execution of POSIX programs with DiOS. - Petr Rockai; Zuzana Baranová; Jan Mrázek; Katarína Kejstová; Jiri Barnat (Softw. Syst. Model., 2021)

DivSIM , an interactive simulator for LLVM bitcode. - Petr Rockai; Jiri Barnat (Int. J. Softw. Tools Technol. Transf., 2022)

RoFIOS - Flexible Full-Stack Software Solution for Metamorphic Robots. - Jan Mrázek; Jiri Barnat (CASE, 2023)

Fault-Tolerant and System-Wide Communication for Metamorphic Robots. - Jan Mrázek; Vladimír Chlup; Jiri Barnat (CASE, 2023)

Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics. - Jan Mrázek; Patrick Ondika; Ivana Cerná; Jiri Barnat (ICRA, 2023)

Tree-Based Reconfiguration of Metamorphic Robots. - Patrick Ondika; Jan Mrázek; Jiri Barnat (IROS, 2024)