| 2024 | IROS | Tree-Based Reconfiguration of Metamorphic Robots. | Patrick Ondika, Jan Mrzek, Jiri Barnat |
| 2023 | ICRA | Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics. | Jan Mrzek, Patrick Ondika, Ivana Cern, Jiri Barnat |
| 2021 | IROS | Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way? | Jan Mrzek, Martin Jons, Jiri Barnat |
| 2020 | QRS | On Symbolic Execution of Decompiled Programs. | Luks Korencik, Petr Rockai, Henrich Lauko, Jiri Barnat |
| 2019 | FMICS | A Simulator for LLVM Bitcode. | Petr Rockai, Jiri Barnat |
| 2019 | IROS | RoFICoM - First Open-Hardware Connector for Metamorphic Robots. | Jan Mrzek, Jiri Barnat |
| 2019 | SEFM | Reproducible Execution of POSIX Programs with DiOS. | Petr Rockai, Zuzana Baranov, Jan Mrzek, Katarna Kejstov, Jiri Barnat |
| 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 |
| 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 |
| 2017 | TACAS | Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution). | Jan Mrzek, Martin Jons, Vladimr Still, Henrich Lauko, Jiri Barnat |
| 2016 | EuroPar | Parametric Multi-step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components. | Stefano Aldegheri, Jiri Barnat, Nicola Bombieri, Federico Busato, Milan Ceska |
| 2016 | SAC | On verifying C++ programs with probabilities. | Jiri Barnat, Ivana Cern, Petr Rockai, Vladimr Still, Kristna Zkopcanov |
| 2016 | SEFM | Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. | Jaroslav Bendk, Nikola Benes, Jiri Barnat, Ivana Cern |
| 2016 | SEFM | LTL Parameter Synthesis of Parametric Timed Automata. | Peter Bezdek, Nikola Benes, Jiri Barnat, Ivana Cern |
| 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 |
| 2015 | SOFSEM | Quo Vadis Explicit-State Model Checking. | Jiri Barnat |
| 2014 | ICTAC | On Clock-Aware LTL Properties of Timed Automata. | Peter Bezdek, Nikola Benes, Vojtech Havel, Jiri Barnat, Ivana Cern |
| 2014 | PDP | Model Checking Parallel Programs with Inputs. | Jiri Barnat, Petr Bauch, Vojtech Havel |
| 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 |
| 2012 | SEFM | Checking Sanity of Software Requirements. | Jiri Barnat, Petr Bauch, Lubos Brim |
| 2012 | TASE | Executing Model Checking Counterexamples in Simulink. | Jiri Barnat, Lubos Brim, Jan Beran, Tomas Kratochvila, Italo R. Oliveira |
| 2010 | ICPADS | Employing Multiple CUDA Devices to Accelerate LTL Model Checking. | Jiri Barnat, Petr Bauch, Lubos Brim, Milan Ceska |
| 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 |
| 2009 | ICPADS | CUDA Accelerated LTL Model Checking. | Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr |
| 2008 | ATVA | DiVinE Multi-Core - A Parallel LTL Model-Checker. | Jiri Barnat, Lubos Brim, Petr Rockai |
| 2008 | FMICS | Local Quantitative LTL Model Checking. | Jiri Barnat, Lubos Brim, Ivana Cern, Milan Ceska, Jana Tumova |
| 2008 | FMICS | Can Flash Memory Help in Model Checking? | Jiri Barnat, Lubos Brim, Stefan Edelkamp, Damian Sulewski, Pavel Simecek |
| 2008 | ISoLA | Squeeze All the Power Out of Your Hardware to Verify Your Software!. | Jiri Barnat, Lubos Brim |
| 2008 | TACAS | Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. | Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber |
| 2007 | CAV | I/O Efficient Accepting Cycle Detection. | Jiri Barnat, Lubos Brim, Pavel Simecek |
| 2007 | ICECCS | Parallel Model Checking and the FMICS-jETI Platform. | Jiri Barnat, Lubos Brim, Martin Leucker |
| 2006 | CAV | DiVinE - A Tool for Distributed Verification. | Jiri Barnat, Lubos Brim, Ivana Cern, Pavel Moravec, Petr Rockai, Pavel Simecek |
| 2006 | FMICS | Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. | Jiri Barnat, Pavel Moravec |