LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. - Jiri Barnat; Lubos Brim; Vojtech Havel (ACSD, 2013)

DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. - Jiri Barnat; Lubos Brim; Vojtech Havel; Jan Havlícek; Jan Kriho; Milan Lenco; Petr Rockai; Vladimír Still; Jirí Weiser (CAV, 2013)

Temporal Verification of Simulink Diagrams. - Jiri Barnat; Petr Bauch; Vojtech Havel (HASE, 2014)

On Clock-Aware LTL Properties of Timed Automata. - Peter Bezdek; Nikola Benes; Vojtech Havel; Jiri Barnat; Ivana Cerná (ICTAC, 2014)

LTL Model Checking of LLVM Bitcode with Symbolic Data. - Petr Bauch; Vojtech Havel; Jiri Barnat (MEMICS, 2014)

Model Checking Parallel Programs with Inputs. - Jiri Barnat; Petr Bauch; Vojtech Havel (PDP, 2014)

LTL Model Checking of Parametric Timed Automata. - Peter Bezdek; Nikola Benes; Vojtech Havel; Jiri Barnat; Ivana Cerná (CoRR, 2014)

Accelerating temporal verification of Simulink diagrams using satisfiability modulo theories. - Petr Bauch; Vojtech Havel; Jiri Barnat (Softw. Qual. J., 2016)

Control Explicit-Data Symbolic Model Checking. - Petr Bauch; Vojtech Havel; Jiri Barnat (ACM Trans. Softw. Eng. Methodol., 2016)

P4Testgen: An Extensible Test Oracle For P4. - Fabian Ruffy; Jed Liu; Prathima Kotikalapudi; Vojtech Havel; Rob Sherwood; Vlad Dubina; Volodymyr Peschanenko; Nate Foster; Anirudh Sivaraman (CoRR, 2022)

P4Testgen: An Extensible Test Oracle For P4-16. - Fabian Ruffy; Jed Liu; Prathima Kotikalapudi; Vojtech Havel; Hanneli Tavante; Rob Sherwood; Vladyslav Dubina; Volodymyr Peschanenko; Anirudh Sivaraman; Nate Foster (SIGCOMM, 2023)