-
Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories J - Článek v odborném periodikuBAUCH, Petr; Vojtěch HAVEL a Jiří BARNAT. Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories. Software Quality Journal. Springer, 2016, roč. 24, č. 1, s. 37-63. ISSN 0963-9314. Dostupné z: https://doi.org/10.1007/s11219-014-9259-x.Podrobněji: https://is.muni.cz/publication/1205968/cs
-
Control Explicit-Data Symbolic Model Checking J - Článek v odborném periodikuBAUCH, Petr; Vojtěch HAVEL a Jiří BARNAT. Control Explicit-Data Symbolic Model Checking. ACM Transactions on Software Engineering and Methodology. 2016, roč. 25, č. 2, s. 15-62. ISSN 1049-331X. Dostupné z: https://doi.org/10.1145/2888393.Podrobněji: https://is.muni.cz/publication/1352219/cs
-
LTL Model Checking of LLVM Bitcode with Symbolic Data D - Stať ve sborníkuBAUCH, Petr; Vojtěch HAVEL a Jiří BARNAT. LTL Model Checking of LLVM Bitcode with Symbolic Data. Online. In P. Hlineny et al. Proceedings of MEMICS'14. Telc: Springer, 2014, s. 47-59. ISBN 978-3-319-14895-3. Dostupné z: https://doi.org/10.1007/978-3-319-14896-0_5.Podrobněji: https://is.muni.cz/publication/1205966/cs
-
Model Checking Parallel Programs with Inputs D - Stať ve sborníkuBARNAT, Jiří; Petr BAUCH a Vojtěch HAVEL. Model Checking Parallel Programs with Inputs. Online. In Proceedings of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP). Turin: IEEE Computer Society, 2014, s. 756-759. ISSN 1066-6192. Dostupné z: https://doi.org/10.1109/PDP.2014.44.Podrobněji: https://is.muni.cz/publication/1129347/cs
-
On Clock-Aware LTL Properties of Timed Automata D - Stať ve sborníkuBEZDĚK, Peter; Nikola BENEŠ; Vojtěch HAVEL; Jiří BARNAT a Ivana ČERNÁ. On Clock-Aware LTL Properties of Timed Automata. In Gabriel Ciobanu, Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014. Neuveden: Springer International Publishing, 2014, s. 43-60. ISBN 978-3-319-10881-0. Dostupné z: https://doi.org/10.1007/978-3-319-10882-7_4.Podrobněji: https://is.muni.cz/publication/1199016/cs
-
Temporal Verification of Simulink Diagrams D - Stať ve sborníkuBARNAT, Jiří; Petr BAUCH a Vojtěch HAVEL. Temporal Verification of Simulink Diagrams. Online. In P. J. Clarke et al. Proceedings of HASE 2014. Miami: IEEE Computer Society, 2014, s. 81-88. ISBN 978-1-4799-3465-2. Dostupné z: https://doi.org/10.1109/HASE.2014.20.Podrobněji: https://is.muni.cz/publication/1129340/cs
-
DIVINE 3.0 (software) R - SoftwareROČKAI, Petr; Jiří BARNAT; Vladimír ŠTILL; Jiří WEISER; Luboš BRIM; Vojtěch HAVEL; Jan HAVLÍČEK a Jan KRIHO. DIVINE 3.0. 2013.Podrobněji: https://is.muni.cz/publication/1179466/cs
-
DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs D - Stať ve sborníkuBARNAT, Jiří; Luboš BRIM; Vojtěch HAVEL; Jan HAVLÍČEK; Jan KRIHO; Milan LENČO; Petr ROČKAI; Vladimír ŠTILL a Jiří WEISER. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Sharygina, Natasha; Veith, Helmut. Computer Aided Verification 2013. Heidelberg: Springer, 2013, s. 863-868. ISBN 978-3-642-39798-1. Dostupné z: https://doi.org/10.1007/978-3-642-39799-8_60.Podrobněji: https://is.muni.cz/publication/1130026/cs
-
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model D - Stať ve sborníkuBARNAT, Jiří; Luboš BRIM a Vojtěch HAVEL. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. In Juan E. Guerrero. Proceedings of Application of Concurrency to System Design, 2013. Barcelona: IEEE Computer Society, 2013, s. 51-59. ISBN 978-0-7695-5035-0. Dostupné z: https://doi.org/10.1109/ACSD.2013.8.Podrobněji: https://is.muni.cz/publication/1130152/cs