| 2022 | TACAS | LART: Compiled Abstract Execution - (Competition Contribution). | Henrich Lauko, Petr Rockai |
| 2020 | QRS | On Symbolic Execution of Decompiled Programs. | Luks Korencik, Petr Rockai, Henrich Lauko, Jiri Barnat |
| 2019 | FM | Compiling C and C++ Programs for Dynamic White-Box Analysis. | Zuzana Baranov, Petr Rockai |
| 2019 | FM | Model Checking in a Development Workflow: A Study on a Concurrent C++ Hash Table. | Petr Rockai |
| 2019 | FMICS | A Simulator for LLVM Bitcode. | Petr Rockai, Jiri Barnat |
| 2019 | SEFM | Reproducible Execution of POSIX Programs with DiOS. | Petr Rockai, Zuzana Baranov, Jan Mrzek, Katarna Kejstov, Jiri Barnat |
| 2019 | TACAS | Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution). | Henrich Lauko, Vladimr Still, Petr Rockai, Jiri Barnat |
| 2018 | ICTAC | Symbolic Computation via Program Transformation. | Henrich Lauko, Petr Rockai, Jiri Barnat |
| 2017 | ATVA | Model Checking of C and C++ with DIVINE 4. | Zuzana Baranov, Jiri Barnat, Katarna Kejstov, Tades Kucera, Henrich Lauko, Jan Mrzek, Petr Rockai, Vladimr Still |
| 2017 | QRS | Using Off-the-Shelf Exception Support Components in C++ Verification. | Vladimr Still, Petr Rockai, Jiri Barnat |
| 2017 | RV | From Model Checking to Runtime Verification and Back. | Katarna Kejstov, Petr Rockai, Jiri Barnat |
| 2016 | SAC | On verifying C++ programs with probabilities. | Jiri Barnat, Ivana Cern, Petr Rockai, Vladimr Still, Kristna Zkopcanov |
| 2016 | TACAS | DIVINE: Explicit-State LTL Model Checker - (Competition Contribution). | Vladimr Still, Petr Rockai, Jiri Barnat |
| 2015 | SEFM | Techniques for Memory-Efficient Model Checking of C and C++ Code. | Petr Rockai, Vladimr Still, Jiri Barnat |
| 2013 | CAV | DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. | Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlcek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimr Still, Jir Weiser |
| 2012 | FMICS | Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. | Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, Petr Rockai |
| 2010 | SEFM | Parallel Partial Order Reduction with Topological Sort Proviso. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2009 | ICFEM | A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2008 | ATVA | DiVinE Multi-Core - A Parallel LTL Model-Checker. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2006 | CAV | DiVinE - A Tool for Distributed Verification. | Jiri Barnat, Lubos Brim, Ivana Cern, Pavel Moravec, Petr Rockai, Pavel Simecek |