This list of papers is also available as a bibtex file.

2017

Petr Ročkai, Vladimír Štill, Ivana Černá, Jiří Barnat: DiVM: Model checking with LLVM and graph memory. 2017. Preliminary version

Petr Ročkai, Jiří Barnat: A simulator for LLVM bitcode. 2017. Preliminary version.

Vladimír Štill, Petr Ročkai, Jiří Barnat: Using off-the-shelf exception support components in C++ verification. 2017. Preliminary version.

Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, Vladimír Štill: Model checking of C and C++ with DIVINE 4. 2017. Preliminary version.

Katarína Kejstová, Petr Ročkai, Jiří Barnat: From model checking to runtime verification and back. 2017. Preliminary version.

2016

Vladimír Štill, Petr Ročkai, Jiří Barnat: Weak Memory Models as LLVM-to-LLVM Transformations. In Mathematical and Engineering Methods in Computer Science, Revised Selected Papers, Springer International Publishing, 2016, volume 9548 of Lecture notes in computer science.

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

Vladimír Štill: LLVM Transformations for Model Checking. Masarykova univerzita, Fakulta informatiky, Brno, 2016.

Jiří Weiser: TCP vrstva pro verifikační nástroj DIVINE. Masarykova univerzita, Fakulta informatiky, Brno, 2016.

Vladimír Štill, Petr Ročkai, Jiří Barnat: DIVINE: Explicit-State LTL Model Checker. In Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, 2016.

Jan Mrázek: Caching SMT Queries in SymDIVINE. Masarykova univerzita, Fakulta informatiky, Brno, 2016.

Jan Mrázek, Petr Bauch, Henrich Lauko, Jiří Barnat: SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Model Checking Software: 23rd International Symposium, SPIN, Springer International Publishing, 2016.

2015

Petr Ročkai, Vladimír Štill, Jiří Barnat: Techniques for Memory-Efficient Model Checking of C and C++ Code. In Software Engineering and Formal Methods, Springer International Publishing, 2015, volume 9276 of Lecture notes in computer science.

Petr Ročkai: Model checking software. Masaryk University, Faculty of Informatics, Brno, 2015.

Milan Lenčo: Verification of Name Service Cache Daemon with DIVINE Model Checker. Masarykova univerzita, Fakulta informatiky, Brno, 2015.

Kristína Zákopčanová: On Chaining Divine and Prism Model Checkers. Masarykova univerzita, Fakulta informatiky, Brno, 2015.

Jiří Barnat, Petr Ročkai, Vladimír Štill, Jiří Weiser: Fast, dynamically-sized concurrent hash table. In Model checking software (spin 2015), Springer International Publishing, 2015, volume 9232 of Lecture notes in computer science.

2014

Petr Bauch, Vojtěch Havel, Jiří Barnat: LTL model checking of llvm bitcode with symbolic data. In Proceedings of memics’14, elektronická verze “online”; Springer, 2014.

Vojtěch Havel: Generic Platform for Explicit-Symbolic Verification. Masarykova univerzita, Fakulta informatiky, Brno, 2014.

Jiří Barnat, Petr Bauch, Vojtěch Havel: Model Checking Parallel Programs with Inputs. In Parallel, distributed and network-based processing (pdp), 2014 22nd euromicro international conference on, 2014.

Petr Ročkai, Jiří Barnat, Luboš Brim: Model Checking C++ with Exceptions. In Automated verification of critical systems, 2014, AVoCS 2014.

Vladimír Štill, Petr Ročkai, Jiří Barnat: Context-Switch-Directed Verification in DIVINE. In Mathematical and Engineering Methods in Computer Science, Springer International Publishing, 2014, volume 8934 of Lecture notes in computer science.

2013

Vladimír Štill: State Space Compression for the DiVinE Model Checker. Masarykova univerzita, Fakulta informatiky, Brno, 2013.

Jiří Weiser: Dynamicky rostoucí sdílená hašovací tabulka pro DiVinE. Masarykova univerzita, Fakulta informatiky, Brno, 2013.

Jan Havlíček: Untimed LTL Model Checking of Timed Automata. Masarykova univerzita, Fakulta informatiky, Brno, 2013.

Jiří Barnat, Jan Havlíček, Petr Ročkai: Distributed ltl model checking with hash compaction. In Electronic notes in theoretical computer science, volume 296, tištěná verze “print”; Elsevier Science, 2013.

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

Jiří Barnat, Luboš Brim, Vojtěch Havel: LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. In Application of Concurrency to System Design (ACSD), IEEE, 2013.

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

2012

Jiří Barnat, Luboš Brim, Petr Ročkai: Towards ltl model checking of unmodified thread-based c & c++ programs. In NASA formal methods: 4th international symposium, nfm 2012, norfolk, va, usa, april 3-5, 2012. proceedings, Springer Berlin Heidelberg, 2012.

Jiří Barnat, Luboš Brim, Petr Ročkai: On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. In Science of Computer Programming, Elsevier North-Holland, Inc., 2012.

Vojtěch Havel: Relaxed Memory Models in DiVinE. Masarykova univerzita, Fakulta informatiky, Brno, 2012.

2010

Petr Ročkai: Partial Order Reduction in Parallel Model Checking. Masarykova univerzita, Fakulta informatiky, Brno, 2010.

Jiří Barnat, Luboš Brim, Petr Ročkai: Scalable Shared Memory LTL Model Checking. In International Journal on Software Tools for Technology Transfer (STTT), 2010.

Jiří Barnat, Luboš Brim, David Šafránek: High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker. In Briefings in Bioinformatics, 2010.

Jiří Barnat, Jakub Chaloupka, Jaco Pol: Distributed Algorithms for SCC Decomposition. In Journal of Logic and Computation, 2010.

Jiří Barnat, Luboš Brim, Petr Ročkai: Parallel Partial Order Reduction with Topological Sort Proviso. In Proceeding of SEFM 2010, IEEE Computer Society Press, 2010.

Jiří Barnat, Luboš Brim, David Šafránek, Martin Vejnár: Parameter Scanning by Parallel Model Checking with Applications in Systems Biology. In Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010), IEEE, 2010.

Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka: Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In 16th International Conference on Parallel and Distributed Systems (ICPADS 2010), IEEE, 2010.

Jiří Barnat, Luboš Brim, Milan Češka, Petr Ročkai: DiVinE: Parallel Distributed Model Checker. In Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology, IEEE, 2010.

2008

Petr Ročkai: Multi-Threaded Nested DFS. Masarykova univerzita, Fakulta informatiky, Brno, 2008.