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

Scalable Multi-core LTL Model-Checking. - Jiri Barnat; Lubos Brim; Petr Rockai (SPIN, 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)

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

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

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

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)

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

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)

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

Context-Switch-Directed Verification in DIVINE. - Vladimír Still; Petr Rockai; Jiri Barnat (MEMICS, 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)

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

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

DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). - Vladimír Still; Petr Rockai; Jiri Barnat (TACAS, 2016)

Model checking C++ programs with exceptions. - Petr Rockai; Jiri Barnat; Lubos Brim (Sci. Comput. Program., 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)

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)

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

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

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

Compiling C and C++ Programs for Dynamic White-Box Analysis. - Zuzana Baranová; Petr Rockai (FM Workshops (1), 2019)

Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table. - Petr Rockai (FM Workshops (1), 2019)

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

String Abstraction for Model Checking of C Programs. - Agostino Cortesi; Henrich Lauko; Martina Olliaro; Petr Rockai (SPIN, 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)

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

LART: Compiled Abstract Execution - (Competition Contribution). - Henrich Lauko; Petr Rockai (TACAS (2), 2022)

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

Verification of Programs Sensitive to Heap Layout. - Henrich Lauko; Lukás Korencik; Petr Rockai (ACM Trans. Softw. Eng. Methodol., 2022)