Vojtěch Havel

2016

Petr Bauch, Vojtěch Havel, and Jiří Barnat:
Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories,
Software Quality Journal, 2016. [bibtex, url]

2014

Vojtěch Havel:
Generic Platform for Explicit-Symbolic Verification,
Master’s Thesis, 2014. [bibtex, pdf, url]

Petr Bauch, Vojtěch Havel, and Jiří Barnat:
LTL Model Checking of LLVM Bitcode with Symbolic Data,
Proceedings of MEMICS’14, Springer, 2014, 47-59. [bibtex, url]

Jiří Barnat, Petr Bauch, and Vojtěch Havel:
Model Checking Parallel Programs with Inputs,
Parallel, Distributed and Network-Based Processing (PDP), 2014 22nd Euromicro International Conference on, 2014, 756-759. [bibtex, url]

Peter Bezděk, Nikola Beneš, Vojtěch Havel, Jiří Barnat, and Ivana Černá:
On Clock-Aware LTL properties of Timed Automata,
International Colloquium on Theoretical Aspects of Computing (ICTAC), Springer, 2014, volume 8687 of LNCS, 46–60. [bibtex]

Jiří Barnat, Petr Bauch, and Vojtěch Havel:
Temporal Verification of Simulink Diagrams,
Proceedings of HASE 2014, IEEE Computer Society, 2014, 81-88. [bibtex]

2013

Jiří Barnat, Luboš Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenčo, Petr Ročkai, Vladimír Štill, and Jiří Weiser:
DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs,
Computer Aided Verification, Springer Berlin Heidelberg, 2013, volume 8044 of Lecture Notes in Computer Science, 863–868. [bibtex, url]

Jiří Barnat, Luboš Brim, and Vojtěch Havel:
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model,
Application of Concurrency to System Design (ACSD), IEEE, 2013, 51–59. [bibtex, url]

2012

Vojtěch Havel:
Relaxed Memory Models in DiVinE,
Bachelor’s Thesis, 2012. [bibtex, pdf, url]