SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. - Jan Mrázek; Petr Bauch; Henrich Lauko; Jiri Barnat (SPIN, 2016)

Model Checking of C and C++ with DIVINE 4. - Zuzana Baranová; Jiri Barnat; Katarína Kejstová; Tadeás Kucera; Henrich Lauko; Jan Mrázek; Petr Rockai; Vladimír Still (ATVA, 2017)

Optimizing and Caching SMT Queries in SymDIVINE - (Competition Contribution). - Jan Mrázek; Martin Jonás; Vladimír Still; Henrich Lauko; Jiri Barnat (TACAS (2), 2017)

Symbolic Computation via Program Transformation. - Henrich Lauko; Petr Rockai; Jiri Barnat (ICTAC, 2018)

String Abstraction for Model Checking of C Programs. - Agostino Cortesi; Henrich Lauko; Martina Olliaro; Petr Rockai (SPIN, 2019)

Extending DIVINE with Symbolic Verification Using SMT - (Competition Contribution). - Henrich Lauko; Vladimír Still; Petr Rockai; Jiri Barnat (TACAS (3), 2019)

On Symbolic Execution of Decompiled Programs. - Lukás Korencik; Petr Rockai; Henrich Lauko; Jiri Barnat (QRS, 2020)

From Spot 2.0 to Spot 2.10: What's New? - Alexandre Duret-Lutz; Etienne Renault; Maximilien Colange; Florian Renkin; Alexandre Gbaguidi Aisse; Philipp Schlehuber-Caissier; Thomas Medioni; Antoine Martin; Jérôme Dubois; Clément Gillard; Henrich Lauko (CAV (2), 2022)

LART: Compiled Abstract Execution - (Competition Contribution). - Henrich Lauko; Petr Rockai (TACAS (2), 2022)

On the Optimization of Equivalent Concurrent Computations. - Henrich Lauko; Lukás Korencik; Peter Goodman (CoRR, 2022)

Verification of Programs Sensitive to Heap Layout. - Henrich Lauko; Lukás Korencik; Petr Rockai (ACM Trans. Softw. Eng. Methodol., 2022)