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)

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

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)

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

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

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)

Automatic Test Generation for Haskell Programming Assignments. - Vladimír Still (ITiCSE, 2020)