| 2020 | ITiCSE | Automatic Test Generation for Haskell Programming Assignments. | Vladimr Still |
| 2019 | SEFM | Local Nontermination Detection for Parallel C++ Programs. | Vladimr Still, Jiri Barnat |
| 2019 | TACAS | Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution). | Henrich Lauko, Vladimr Still, Petr Rockai, Jiri Barnat |
| 2018 | ICFEM | Model Checking of C++ Programs Under the x86-TSO Memory Model. | Vladimr Still, 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 | TACAS | Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution). | Jan Mrzek, Martin Jons, Vladimr Still, Henrich Lauko, 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 |