papers
This list of papers is also available as a bibtex file.
2022
- Ročkai, J. Barnat: DivSIM, an interactive simulator for LLVM bitcode
- Lauko, P. Ročkai: LART: Compiled abstract execution: (Competition contribution)
2021
Petr Ročkai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiří Barnat:
Reproducible execution of POSIX programs with DiOS. In Software and Systems Modeling, 2021.
2020
- Lauko, M. Olliaro, A. Cortesi, P. Ročkai: Abstracting strings for model checking of C programs
- Baranová, P. Ročkai: Compiling C and C++ programs for dynamic white-box analysis
- Korencik, P. Rockai, H. Lauko, J. Barnat: On symbolic execution of decompiled programs
2019
Katarína Kejstová:
Model checking with system call traces. Masarykova univerzita, Fakulta informatiky, Brno, 2019.
Petr Ročkai, Zuzana Baranová, Jan Mrázek, Katarína Kejstová, Jiří Barnat:
Reproducible execution of POSIX programs with DiOS. In Software engineering and formal methods, Springer, 2019, LNCS.
Petr Ročkai, Jiří Barnat:
A simulator for LLVM bitcode. In Formal methods for industrial critical systems, Springer, 2019.
- Cortesi, H. Lauko, M. Olliaro, P. Ročkai: String abstraction for model checking of C programs
- Lauko, V. Štill, P. Ročkai, J. Barnat: Extending divine with symbolic verification using smt: (Competition contribution)
2018
Petr Ročkai, Vladimír Štill, Ivana Černá, Jiří Barnat:
DiVM: Model checking with LLVM and graph memory. In Journal of Systems and Software, Elsevier, 2018.
- Lauko, P. Ročkai, J. Barnat: Symbolic computation via program transformation
Vladimír Štill, Jiří Barnat:
Model Checking of C++ Programs Under the x86-TSO Memory Model. In Formal methods and software engineering, Springer International Publishing, 2018.
2017
Petr Ročkai, Jiří Barnat:
A simulator for LLVM bitcode. In CoRR, 2017.
Vladimír Štill, Petr Ročkai, Jiří Barnat:
Using off-the-shelf exception support components in C++ verification. In IEEE international conference on software quality, reliability and security (qrs), 2017.
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. In Automated technology for verification and analysis, ATVA, Springer, 2017, volume 10482 of LNCS.
Katarína Kejstová, Petr Ročkai, Jiří Barnat:
From model checking to runtime verification and back. In Runtime verification - 17th international conference, RV 2017, 2017.
2016
Petr Ročkai, Jiří Barnat, Luboš Brim:
Model checking C++ programs with exceptions. In Science of Computer Programming, 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 LNCS.
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 LNCS.
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), Springer International Publishing, 2015, volume 9232 of LNCS.
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 LNCS.
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 LNCS.
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, 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, 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), 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.