ParaDiSe publications with the support of Red Hat

2017

Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill:
Model Checking of C and C++ with DIVINE 4,
International Symposium on Automated Technology for Verification and Analysis (ATVA) (to appear), 2017. [bibtex, paper page]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Using Off-the-Shelf Exception Support Components in C++ Verification,
Software Quality, Reliability & Security (to appear), 2017. [bibtex, paper page]

2016

Jiří Barnat, Ivana Černá, Petr Ročkai, Vladimír Štill, and Kristína Zákopčanová:
On Verifying C++ Programs with Probabilities,
ACM Symposium on Applied Computing, 2016, 1238–1243. [bibtex, url]

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Weak Memory Models as LLVM-to-LLVM Transformations,
Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, Springer International Publishing, 2016, volume 9548 of Lecture Notes in Computer Science, 144–155. [bibtex, pdf, url]

2015

Jiří Barnat, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
Fast, Dynamically-Sized Concurrent Hash Table,
Model Checking Software (SPIN 2015), Springer International Publishing, 2015, volume 9232 of Lecture Notes in Computer Science, 49-65. [bibtex, pdf, url]

2014

Vladimír Štill, Petr Ročkai, and Jiří Barnat:
Context-Switch-Directed Verification in DIVINE,
Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture Notes in Computer Science, 135–146. [bibtex, pdf, url]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Model Checking C++ with Exceptions,
Automated Verification of Critical Systems, 2014. [bibtex, url]

2013

Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, Springer Berlin Heidelberg, 2013, volume 8044 of Lecture Notes in Computer Science, 863–868. [bibtex, url]

Petr Ročkai, Jiří Barnat, and Luboš Brim:
Improved State Space Reductions for LTL Model Checking of C & C++ Programs,
NASA Formal Methods (NFM 2013), Springer, 2013, volume 7871 of LNCS, 1–15. [bibtex]

2010

Jiří Barnat, Luboš Brim, Milan Češka, and Petr Ročkai:
DiVinE: Parallel Distributed Model Checker,
Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, 2010, 4–7. [bibtex, url]