Výpis publikací

ONDIKA, Patrick; Jan MRÁZEK a Jiří BARNAT. Tree-Based Reconfiguration of Metamorphic Robots. Online. In 2024 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). Abu Dhabi: IEEE, 2024, s. 3498-3504. ISBN 979-8-3503-7771-2. Dostupné z: https://doi.org/10.1109/IROS58592.2024.10801396.

MRÁZEK, Jan; Vladimír CHLUP a Jiří BARNAT. Fault-Tolerant and System-Wide Communication for Metamorphic Robots. Online. In 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE). Auckland, New Zealand: IEEE, 2023, s. 1-8. ISBN 979-8-3503-2069-5. Dostupné z: https://doi.org/10.1109/CASE56687.2023.10260364.

MRÁZEK, Jan a Jiří BARNAT. RoFIOS - Flexible Full-Stack Software Solution for Metamorphic Robots. Online. In 2023 IEEE 19th International Conference on Automation Science and Engineering (CASE). Auckland, New Zealand: IEEE, 2023, s. 1-8. ISBN 979-8-3503-2069-5. Dostupné z: https://doi.org/10.1109/CASE56687.2023.10260586.

MRÁZEK, Jan; Patrick ONDIKA; Ivana ČERNÁ a Jiří BARNAT. Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics. Online. In 2023 IEEE International Conference on Robotics and Automation (ICRA). London: IEEE, 2023, s. 11894-11900. ISBN 979-8-3503-2365-8. Dostupné z: https://doi.org/10.1109/ICRA48891.2023.10160352.

ROČKAI, Petr a Jiří BARNAT. DivSIM , an interactive simulator for LLVM bitcode. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. GERMANY: SPRINGER HEIDELBERG, 2022, roč. 24, č. 3, s. 493-510. ISSN 1433-2779. Dostupné z: https://doi.org/10.1007/s10009-022-00659-x.

ROČKAI, Petr; Henrich LAUKO; Vladimír ŠTILL; Zuzana BARANOVÁ; Lukáš KORENČIK; Adam MATOUŠEK; Jiří BARNAT; Jakub ŠÁRNÍK; Jan MRÁZEK; Katarína KEJSTOVÁ a Tadeáš KUČERA. DIVINE 4.4. 2021.

MRÁZEK, Jan; Martin JONÁŠ a Jiří BARNAT. Reconfiguring Metamorphic Robots via SMT: Is It a Viable Way?. Online. In 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). Prague: IEEE, 2021, s. 6935-6940. ISBN 978-1-6654-1714-3. Dostupné z: https://doi.org/10.1109/IROS51168.2021.9636534.

ROČKAI, Petr; Zuzana BARANOVÁ; Jan MRÁZEK; Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible execution of POSIX programs with DiOS. Software & Systems Modeling. Springer, 2021, roč. 20, č. 2, s. 363-382. ISSN 1619-1366. Dostupné z: https://doi.org/10.1007/s10270-020-00837-y.

KORENČIK, Lukáš; Petr ROČKAI; Henrich LAUKO a Jiří BARNAT. On Symbolic Execution of Decompiled Programs. In Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020. Neuveden: IEEE Computer Society, 2020, s. 265-272. ISBN 978-1-7281-8914-7. Dostupné z: https://doi.org/10.1109/QRS51102.2020.00044.

ROČKAI, Petr a Jiří BARNAT. A Simulator for LLVM Bitcode. In K. G. Larsen, T. Willemse. 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019. Scham: Springer Verlag, 2019, s. 127-142. ISBN 978-3-030-27007-0. Dostupné z: https://doi.org/10.1007/978-3-030-27008-7_8.

LAUKO, Henrich; Vladimír ŠTILL; Petr ROČKAI a Jiří BARNAT. Extending DIVINE with Symbolic Verification Using SMT. In Beyer, Dirkand Huisman, Mariekeand Kordon, Fabriceand Steffen, Bernhard. Tools and Algorithms for the Construction and Analysis of Systems. Cham: Springer International Publishing, 2019, s. 204-208. ISBN 978-3-030-17501-6. Dostupné z: https://doi.org/10.1007/978-3-030-17502-3_14.

ŠTILL, Vladimír a Jiří BARNAT. Local Nontermination Detection for Parallel C++ Programs. In Ölveczky P., Salaün G. International Conference on Software Engineering and Formal Methods. Cham: Springer, 2019, s. 373-390. ISBN 978-3-030-30445-4. Dostupné z: https://doi.org/10.1007/978-3-030-30446-1_20.

ROČKAI, Petr; Zuzana BARANOVÁ; Jan MRÁZEK; Katarína KEJSTOVÁ a Jiří BARNAT. Reproducible Execution of POSIX Programs with DiOS. In Peter Csaba Ölveczky and Gwen Salaün. Software Engineering and Formal Methods. 17th ed. Cham: Springer International Publishing, 2019, s. 333-349. ISBN 978-3-030-30445-4. Dostupné z: https://doi.org/10.1007/978-3-030-30446-1_18.

MRÁZEK, Jan a Jiří BARNAT. RoFICoM - First Open-Hardware Connector for Metamorphic Robots. In 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). Neuveden: IEEE, 2019, s. 2720-2725. ISBN 978-1-7281-4004-9. Dostupné z: https://doi.org/10.1109/IROS40897.2019.8968167.

ROČKAI, Petr; Vladimír ŠTILL; Ivana ČERNÁ a Jiří BARNAT. DiVM: Model checking with LLVM and graph memory. Journal of Systems and Software. Elsevier, 2018, roč. 143, Oct, s. 1-13. ISSN 0164-1212. Dostupné z: https://doi.org/10.1016/j.jss.2018.04.026.

ŠTILL, Vladimír a Jiří BARNAT. Model Checking of C++ Programs Under the x86-TSO Memory Model. In Jing Sun, Meng Sun. Formal Methods and Software Engineering. Cham: Springer, 2018, s. 124-140. ISBN 978-3-030-02449-9. Dostupné z: https://doi.org/10.1007/978-3-030-02450-5_8.

BEZDĚK, Peter; Nikola BENEŠ; Ivana ČERNÁ a Jiří BARNAT. On clock-aware LTL parameter synthesis of timed automata. Journal of Logical and Algebraic Methods in Programming. ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH: Elsevier, 2018, roč. 99, Oct, s. 114-142. ISSN 2352-2208. Dostupné z: https://doi.org/10.1016/j.jlamp.2018.05.004.

LAUKO, Henrich; Petr ROČKAI a Jiří BARNAT. Symbolic Computation via Program Transformation. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018, s. 313-332. ISBN 978-3-030-02507-6. Dostupné z: https://doi.org/10.1007/978-3-030-02508-3_17.

BRIM, Luboš; Jiří BARNAT; David ŠAFRÁNEK; Nikola BENEŠ; Martin DEMKO; Samuel PASTVA a Matej HAJNAL. Detecting Attractors in Biological Models with Uncertain Parameters. In Jérôme Feret and Heinz Koeppl. Computational Methods in Systems Biology. CMSB 2017. LNCS 10545. Cham: Springer International Publishing, 2017, s. 40-56. ISBN 978-3-319-67470-4. Dostupné z: https://doi.org/10.1007/978-3-319-67471-1_3.

KEJSTOVÁ, Katarína; Petr ROČKAI a Jiří BARNAT. From Model Checking to Runtime Verification and Back. In Shuvendu Lahiri, Giles Reger. Runtime Verification - 17th International Conference, RV 2017. neuvedeno: Springer, 2017, s. 225-240. ISBN 978-3-319-67530-5. Dostupné z: https://doi.org/10.1007/978-3-319-67531-2_14.

BARANOVÁ, Zuzana; Jiří BARNAT; Katarína KEJSTOVÁ; Tadeáš KUČERA; Henrich LAUKO; Jan MRÁZEK; Petr ROČKAI a Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Cham: Springer International Publishing, 2017, s. 201-207. ISBN 978-3-319-68166-5. Dostupné z: https://doi.org/10.1007/978-3-319-68167-2_14.

MRÁZEK, Jan; Martin JONÁŠ; Vladimír ŠTILL; Henrich LAUKO a Jiří BARNAT. Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution). In Axel Legay, Tiziana Margaria. Tools and Algorithms for the Construction and Analysis of Systems, 23rd International Conference, TACAS 2017, Part II. Berlin, Heidelberg: Springer, 2017, s. 390-393. ISBN 978-3-662-54579-9. Dostupné z: https://doi.org/10.1007/978-3-662-54580-5_29.

ALDEGHERI, Stefano; Jiří BARNAT; Nicola BOMBIERI; Federico BUSATO a Milan ČEŠKA. Parametric multi-step scheme for GPU-accelerated graph decomposition into strongly connected components. In 22nd International Conference on Parallel and Distributed Computing, Euro-Par 2016. Cham: Springer Verlag, 2017, s. 519-531. ISBN 978-3-319-58942-8. Dostupné z: https://doi.org/10.1007/978-3-319-58943-5_42.

ŠTILL, Vladimír; Petr ROČKAI a Jiří BARNAT. Using Off-the-Shelf Exception Support Components in C++ Verification. Online. In IEEE International Conference on Software Quality, Reliability and Security - QRS 2017. Neuveden: IEEE, 2017, s. 54-64. ISBN 978-1-5386-0592-9. Dostupné z: https://doi.org/10.1109/QRS.2017.15.

BAUCH, 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.

BARNAT, Jiří; Petr BAUCH; Nikola BENEŠ; Luboš BRIM; Jan BERAN a Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing. 2016, roč. 28, č. 1, s. 45-63. ISSN 0934-5043. Dostupné z: https://doi.org/10.1007/s00165-015-0348-9.

BAUCH, 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.

ŠTILL, Vladimír; Petr ROČKAI a Jiří BARNAT. DIVINE: Explicit-State LTL Model Checker. In M. Chechik and J.-F. Raskin. Proceedings of the 22Nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. New York, NY, USA: Springer-Verlag New York, Inc., 2016, s. 920-922. ISBN 978-3-662-49673-2. Dostupné z: https://doi.org/10.1007/978-3-662-49674-9_60.

BENDÍK, Jaroslav; Nikola BENEŠ; Jiří BARNAT a Ivana ČERNÁ. Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. In Rocco De Nicola, Eva K{\"{u}}hn. Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. Berlin: Lecture Notes in Computer Sciences in Computer Science, 9763, 2016, s. 121-136. ISBN 978-3-319-41590-1. Dostupné z: https://doi.org/10.1007/978-3-319-41591-8_9.

BEZDĚK, Peter; Nikola BENEŠ; Jiří BARNAT a Ivana ČERNÁ. LTL Parameter Synthesis of Parametric Timed Automata. In Rocco De Nicola, Eva K{\"{u}}hn. Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. Berlin: Lecture Notes in Computer Sciences in Computer Science, 9763, 2016, s. 172-187. ISBN 978-3-319-41590-1. Dostupné z: https://doi.org/10.1007/978-3-319-41591-8_12.

ROČKAI, Petr; Jiří BARNAT a Luboš BRIM. Model checking C++ programs with exceptions. Science of Computer Programming. Elsevier B.V., 2016, roč. 128, 15 October 2016, s. 68-85. ISSN 0167-6423. Dostupné z: https://doi.org/10.1016/j.scico.2016.05.007.

BARNAT, Jiří; Ivana ČERNÁ; Petr ROČKAI; Vladimír ŠTILL a Kristína ZÁKOPČANOVÁ. On verifying C++ programs with probabilities. In Sascha Ossowski. Proceedings of the 31st Annual ACM Symposium on Applied Computing. Pisa: ACM New York, NY, USA, 2016, s. 1238-1243. ISBN 978-1-4503-3739-7. Dostupné z: https://doi.org/10.1145/2851613.2851721.

TESAŘOVÁ, Eva; Mária SVOREŇOVÁ; Jiří BARNAT a Ivana ČERNÁ. Optimal observation mode scheduling for systems under temporal constraints. In 2016 American Control Conference (ACC). Boston: IEEE Conference Publications, 2016, s. 1099-1104. ISBN 978-1-4673-8682-1. Dostupné z: https://doi.org/10.1109/ACC.2016.7525062.

MRÁZEK, Jan; Petr BAUCH; Henrich LAUKO a Jiří BARNAT. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Dragan Bošnački and Anton Wijs. Model Checking Software. Neuveden: Springer International Publishing, 2016, s. 208-213. ISBN 978-3-319-32581-1. Dostupné z: https://doi.org/10.1007/978-3-319-32582-8_14.

BENDÍK, Jaroslav; Nikola BENEŠ; Ivana ČERNÁ a Jiří BARNAT. Tunable Online MUS/MSS Enumeration. In Akash Lal, S. Akshay, Saket Saurabh, Sandeep Sen. Foundations of Software Technology and Theoretical Computer Science - 36th International Conference, FSTTCS 2016. 65. vyd. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016, s. 661-673. ISBN 978-3-95977-027-9. Dostupné z: https://doi.org/10.4230/LIPIcs.FSTTCS.2016.50.

ŠTILL, Vladimír; Petr ROČKAI a Jiří BARNAT. Weak Memory Models as LLVM-to-LLVM Transformations. Online. In Jan Kofroň and Tomáš Vojnar. Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop. Neuveden: Springer, 2016, s. 144-155. ISBN 978-3-319-29816-0. Dostupné z: https://doi.org/10.1007/978-3-319-29817-7_13.

BARNAT, Jiří; Petr ROČKAI; Vladimír ŠTILL a Jiří WEISER. Fast, Dynamically-Sized Concurrent Hash Table. In Bernd Fischer, Jaco Geldenhuys. Model Checking Software. Neuveden: Springer International Publishing, 2015, s. 49-65. ISBN 978-3-319-23403-8. Dostupné z: https://doi.org/10.1007/978-3-319-23404-5_5.

BARNAT, Jiří. Quo Vadis Explicit-State Model Checking. In Giuseppe F. Italiano and Tiziana Margaria-Steffen and Jaroslav Pokorný and Jean-Jacques Quisquater and Roger Wattenhofer. SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science. Neuveden: Springer, 2015, s. 46-57. ISBN 978-3-662-46077-1. Dostupné z: https://doi.org/10.1007/978-3-662-46078-8_5.

ROČKAI, Petr; Vladimír ŠTILL a Jiří BARNAT. Techniques for Memory-Efficient Model Checking of C and C++ Code. In Radu Calinescu, Bernhard Rumpe. Software Engineering and Formal Methods. Neuveden: Springer International Publishing, 2015, s. 268-282. ISBN 978-3-319-22968-3. Dostupné z: https://doi.org/10.1007/978-3-319-22969-0_19.

ŠTILL, Vladimír; Petr ROČKAI a Jiří BARNAT. Context-Switch-Directed Verification in DIVINE. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. Mathematical and Engineering Methods in Computer Science. Neuveden: Springer International Publishing, 2014, s. 135-146. ISBN 978-3-319-14895-3. Dostupné z: https://doi.org/10.1007/978-3-319-14896-0_12.

BAUCH, 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.

BEZDĚK, Peter; Nikola BENEŠ; Jiří BARNAT a Ivana ČERNÁ. LTL Model Checking of Parametric Timed Automata. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. MEMICS 2014. Brno, Czech Republic: NOVPRESS, 2014, s. 28-39. ISBN 978-80-214-5022-6.

ROČKAI, Petr; Jiří BARNAT a Luboš BRIM. Model Checking C++ with Exceptions. Electronic Communications of the EASST. 2014, roč. 70, Listopad, s. 1-15. ISSN 1863-2122. Dostupné z: https://doi.org/10.14279/tuj.eceasst.70.983.

BARNAT, 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.

BEZDĚ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.

BARNAT, 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.

BARNAT, Jiří; Nikola BENEŠ; Tomáš BUREŠ; Ivana ČERNÁ; Tomáš KEZNIKL a František PLÁŠIL. Towards Verification of Ensemble Based Component Systems. In José Luiz Fiadeiro, Zhiming Liu, Jinyun Xue. Formal Aspects of Component Software. Neuveden: Springer International Publishing, 2014, s. 41-60. ISBN 978-3-319-07601-0. Dostupné z: https://doi.org/10.1007/978-3-319-07602-7_5.

BARNAT, Jiří; Nikola BENEŠ; Ivana ČERNÁ a Zuzana PETRUCHOVÁ. DCCL: Verification of Component Systems with Ensembles. In CBSE '13 Proceedings of the 16th International ACM Sigsoft symposium on Component-based software engineering. New York, NY, USA: ACM, 2013, s. 43-52. ISBN 978-1-4503-2122-8. Dostupné z: https://doi.org/10.1145/2465449.2465453.

BARNAT, Jiří; Jan HAVLÍČEK a Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science, 2013, s. 79-93. ISSN 1571-0661. Dostupné z: https://doi.org/10.1016/j.entcs.2013.07.006.

ROČKAI, Petr; Jiří BARNAT; Vladimír ŠTILL; Jiří WEISER; Luboš BRIM; Vojtěch HAVEL; Jan HAVLÍČEK a Jan KRIHO. DIVINE 3.0. 2013.

BARNAT, 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.

YORDANOV, Boyan; Jana TŮMOVÁ; Ivana ČERNÁ; Jiří BARNAT a Calin BELTA. Formal analysis of piecewise affine systems through formula-guided refinement. Automatica. Elsevier, 2013, roč. 49, č. 1, s. 261-266. ISSN 0005-1098. Dostupné z: https://doi.org/10.1016/j.automatica.2012.09.027.

ROČKAI, Petr; Jiří BARNAT a Luboš BRIM. Improved State Space Reductions for LTL Model Checking of C & C++ Programs. In Guillaume Brat, Neha Rungta, Arnaud Venet. NASA Formal Methods 2013. Neuveden: Springer, 2013, s. 1-15. ISBN 978-3-642-38087-7. Dostupné z: https://doi.org/10.1007/978-3-642-38088-4_1.

BARNAT, 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.

SVOREŇOVÁ, Mária; Jana TŮMOVÁ; Jiří BARNAT a Ivana ČERNÁ. Attraction-Based Receding Horizon Path Planning with Temporal Logic Constraints. Online. In Proceedings of the 51st IEEE Conference on Decision and Control. Neuveden: Omnipress for the IEEE Control Systems Society, 2012, s. 6749-6754. ISBN 978-1-4673-2066-5. Dostupné z: https://doi.org/10.1109/CDC.2012.6426041.

BARNAT, Jiří; Petr BAUCH; Luboš BRIM a Milan ČEŠKA. Designing Fast LTL Model Checking Algorithms for Many-core GPUs. Journal of Parallel and Distributed Computing. Elsevier, 2012, roč. 72, č. 9, s. 1083-1097. ISSN 0743-7315. Dostupné z: https://doi.org/10.1016/j.jpdc.2011.10.015.

BARNAT, Jiří; Luboš BRIM; Jan BERAN; Tomáš KRATOCHVÍLA a Italo Romani DE OLIVEIRA. Executing Model Checking Counterexamples in Simulink. In Tiziana Margaria, Zongyan Qiu, and Hongli Yang. IEEE Sixth International Symposium on Theoretical Aspects of Software Engineering. Neuveden: IEEE Computer Society, 2012, s. 245-248. ISBN 978-0-7695-4751-0.

BARNAT, Jiří; Petr BAUCH a Luboš BRIM. Checking Sanity of Software Requirements. In George Eleftherakis , Mike Hinchey and Mike Holcombe. Proceedings of the 10th International Conference on Software Engineering and Formal Methods. Thessaloniki: Springer, 2012, s. 48-62. ISBN 978-3-642-33825-0. Dostupné z: https://doi.org/10.1007/978-3-642-33826-7_4.

BARNAT, Jiří; Luboš BRIM; Adam KREJČÍ; Adam STRECK; David ŠAFRÁNEK; Martin VEJNÁR a Tomáš VEJPUSTEK. On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Transactions on Computational Biology and Bioinformatics. Los Alamitos: IEEE Computer Society, 2012, roč. 9, č. 3, s. 693-705. ISSN 1545-5963. Dostupné z: https://doi.org/10.1109/TCBB.2011.110.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Science of Computer Programming. Elsevier, 2012, roč. 77, č. 12, s. 1272-1288. ISSN 0167-6423. Dostupné z: https://doi.org/10.1016/j.scico.2011.03.001.

YORDANOV, Boyan; Jana TŮMOVÁ; Ivana ČERNÁ; Jiří BARNAT a Calin BELTA. Temporal Logic Control of Discrete-Time Piecewise Affine Systems. IEEE Transactions on Automatic Control. PISCATAWAY, 2012, roč. 57, č. 6, s. 1491-1504. ISSN 0018-9286. Dostupné z: https://doi.org/10.1109/TAC.2011.2178328.

BARNAT, Jiří; Ivana ČERNÁ a Jana TŮMOVÁ. Timed Automata Approach to Verification of Systems with Degradation. In MEMICS 2011. LNCS 7119. Heidelberg: Springer, 2012, s. 84 - 93. ISBN 978-3-642-25928-9. Dostupné z: https://doi.org/10.1007/978-3-642-25929-6_8.

BARNAT, Jiří; Jan BERAN; Luboš BRIM; Tomáš KRATOCHVÍLA a Petr ROČKAI. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In Mariëlle Stoelinga, Ralf Pinger. Formal Methods for Industrial Critical Systems (FMICS 2012). Berlin: Springer Berlin Heidelberg, 2012, s. 78--92. ISBN 978-3-642-32468-0. Dostupné z: https://doi.org/10.1007/978-3-642-32469-7_6.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In NASA Formal Methods. Berlin: Springer-Verlag Berlin Heidelberg, 2012, s. 252-266. ISBN 978-3-642-28890-6. Dostupné z: https://doi.org/10.1007/978-3-642-28891-3_25.

BARNAT, Jiří; Ivana ČERNÁ a Jana TŮMOVÁ. Verification of Systems with Degradation. Computing and Informatics. 2012, roč. 31, č. 3, s. 507-530. ISSN 1335-9150.

BARNAT, Jiří; Petr BAUCH; Luboš BRIM a Milan ČEŠKA. Computing Optimal Cycle Mean in Parallel on CUDA. Electronic Proceedings in Theoretical Computer Science. 2011, roč. 72, č. 2011, s. 68-83. ISSN 2075-2180. Dostupné z: https://doi.org/10.4204/EPTCS.72.8.

BARNAT, Jiří; Petr BAUCH; Luboš BRIM a Milan ČEŠKA. Computing Strongly Connected Components in Parallel on CUDA. In Proceedings of 25th IEEE International Parallel & Distributed Processing Symposium. Anchorage, AK: IEEE Computer Society, 2011, s. 544 - 555. ISBN 978-1-61284-372-8.

BARNAT, Jiří; Jakub CHALOUPKA a Jaco VAN DE POL. Distributed Algorithms for SCC Decomposition. Journal of Logic and Computation. Oxford University Press, 2011, roč. 21, č. 1, s. 23-44. ISSN 0955-792X. Dostupné z: https://doi.org/10.1093/logcom/exp003.

EDELKAMP, Stefan; Damian SULEWSKI; Jiří BARNAT; Luboš BRIM a Pavel ŠIMEČEK. Flash memory efficient LTL model checking. Science of Computer Programming. Elsevier, 2011, roč. 76, č. 2, s. 136--157. ISSN 0167-6423. Dostupné z: https://doi.org/10.1016/j.scico.2010.03.005.

BRIM, Luboš a Jiří BARNAT. Platform Dependent Verification: On Engineering Verification Tools for 21st Century. Electronic Proceedings in Theoretical Computer Science. 2011, roč. 72, č. 2011, s. 1-12. ISSN 2075-2180. Dostupné z: https://doi.org/10.4204/EPTCS.72.1.

TŮMOVÁ, Jana; Boyan YORDANOV; Calin BELTA; Ivana ČERNÁ a Jiří BARNAT. A Symbolic Approach to Controlling Piecewise Affine Systems. In Proceedings of of the 49th IEEE Conference on Decision and Control (CDC). Neuveden: Omnipress for IEEE Control Systems Society, 2010, s. 4230-4235. ISBN 978-1-4244-7744-9.

BARNAT, Jiří; Luboš BRIM; Milan ČEŠKA a Petr ROČKAI. DiVinE: Parallel Distributed Model Checker (Tool paper). In Proceedings of joint HiBi/PDMC workshop (HiBi/PDMC 2010). 2010, 4 s.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. DiVinE 2.4. 2010.

BARNAT, Jiří; Petr BAUCH; Luboš BRIM a Milan ČEŠKA. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In Proceedings of 16th International Conference on Parallel and Distributed Systems (ICPADS 2010). Neuveden: IEEE Computer Society, 2010, s. 259-266. ISBN 978-0-7695-4307-9.

YORDANOV, Boyan; Jana TŮMOVÁ; Calin BELTA; Ivana ČERNÁ a Jiří BARNAT. Formal Analysis of Piecewise Affine Systems through Formula-Guided Refinement. In Proceedings of of the 49th IEEE Conference on Decision and Control (CDC). Neuveden: Omnipress for IEEE Control Systems Society, 2010, s. 5899-5904. ISBN 978-1-4244-7744-9.

BARNAT, Jiří; Luboš BRIM a David ŠAFRÁNEK. High-performance analysis of biological systems dynamics with the DiVinE model checker. Briefings in Bioinformatics. Oxford (UK): Oxford University Press, 2010, roč. 11, č. 3, s. 301-312. ISSN 1467-5463.

BARNAT, Jiří; Luboš BRIM; Petr BAUCH a Milan ČEŠKA. MWC-DiVinE. 2010.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos: IEEE Computer Society Press, 2010, s. 222-231. ISBN 978-0-7695-4153-2.

BARNAT, Jiří; Luboš BRIM; David ŠAFRÁNEK a Martin VEJNÁR. Parameter Scanning by Parallel Model Checking with Applications in Systems Biology. In Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology. Los Alamitos: IEEE Computer Society, 2010, s. 95-104. ISBN 978-0-7695-4265-2.

APPL, Jiří; Jiří BARNAT; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE 2.0. 2010.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2010, roč. 12, č. 2, s. 139-153. ISSN 1433-2779. Dostupné z: https://doi.org/10.1007/s10009-010-0136-z.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In Formal Methods and Software Engineering. Germany: Springer Berlin / Heidelberg, 2009, s. 407-425. ISBN 978-3-642-10372-8. Dostupné z: https://doi.org/10.1007/978-3-642-10373-5_21.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Sven DRAŽAN; Jana FABRIKOVÁ; Jan LÁNÍK; David ŠAFRÁNEK a Ma HONGWU. BioDiVinE: A Framework for Parallel Analysis of Biological Models. In Proceedings of 2nd International Workshop on Computational Models for Cell Processes. Neuveden: EPTCS, 2009, s. 31-45. ISSN 2075-2180.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Sven DRAŽAN; Jana FABRIKOVÁ; Jan LÁNÍK a David ŠAFRÁNEK. BioDiVinE: A Tool for Parallel Analysis of Multi-Affine ODE Models. In Computational Mehotds in Systems Biology: Abstract of the Posters. Pisa: University of Pisa, 2009, s. 1-5, 4 s.

BARNAT, Jiří; Luboš BRIM; Stefan EDELKAMP; Damian SULEWSKI a Pavel ŠIMEČEK. Can Flash Memory Help in Model Checking? In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009, s. 150-165. ISBN 978-3-642-03239-4. Dostupné z: https://doi.org/10.1007/978-3-642-03240-0_14.

BARNAT, Jiří; Luboš BRIM a Pavel ŠIMEČEK. Cluster-Based I/O-Efficient LTL Model Checking. In 24th IEEE/ACM International Conference on Automated Software Engineering. Los Calamitos (California): IEEE Computer Society, 2009, s. 635-639. ISBN 978-0-7695-3891-4.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Sven DRAŽAN; Jana FABRIKOVÁ a David ŠAFRÁNEK. Computational Analysis of Large-Scale Multi-Affine ODE Models. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California): IEEE Computer Society, 2009, s. 81-90. ISBN 978-0-7695-3809-9.

BARNAT, Jiří; Luboš BRIM; Milan ČEŠKA a Tomáš LAMR. CUDA Accelerated LTL Model Checking. In Proceedings of the 15th International Conference on Parallel and Distributed Systems. Neuveden: Roy Sterritt, 2009, s. 34-41. ISBN 978-0-7695-3900-3.

BARNAT, Jiří; Luboš BRIM; Petr BAUCH; Milan ČEŠKA a Tomáš LAMR. DiVinE Cuda. 2009.

ROČKAI, Petr; Jiří BARNAT; Luboš BRIM a Milan ČEŠKA. DiVinE 2.0. 2009.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. DiVinE 2.0: High-Performance Model Checking. In International Workshop on High Performance Computational Systems Biology. Los Alamitos (California): IEEE Computer Society, 2009, s. 31-32. ISBN 978-0-7695-3809-9.

BARNAT, Jiří; Luboš BRIM a Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science. 2009, roč. 14, Prosinec, s. 107--111. ISSN 2075-2180.

VERSTOEP, Kees; Henri E. BAL; Jiří BARNAT a Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE, 2009, s. 201-212. ISBN 978-1-4244-3751-1.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009, s. 53-68. ISBN 978-3-642-03239-4. Dostupné z: https://doi.org/10.1007/978-3-642-03240-0_8.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Sven DRAŽAN; Jana FABRIKOVÁ a David ŠAFRÁNEK. On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking. Theoretical Computer Science. 2009, roč. 2009, č. 410, s. 3128-3148, 20 s. ISSN 0304-3975.

BARNAT, Jiří; Ivana ČERNÁ a Jana TŮMOVÁ. Quantitative Model Checking of Systems with Degradation. In 2009 Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos (California): IEEE Computer Society, 2009, s. 21-30. ISBN 978-0-7695-3808-2.

BARNAT, Jiří; Luboš BRIM; Stefan EDELKAMP; Damian SULEWSKI a Pavel ŠIMEČEK. Can Flash Memory Help in Model Checking? In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla: ERCIM, 2008, s. 159-174.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Pavel ŠIMEČEK. DiVinE Cluster. 2008.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008, s. 234-239. ISBN 978-3-540-88386-9.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Sven DRAŽAN a David ŠAFRÁNEK. From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks. In Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation. Budapest: Ivana Cerna and Gerald Luettgen, 2008, s. 83-96, 15 s. ISSN 1571-0661.

BARNAT, Jiří; Jakub CHALOUPKA a Jaco VAN DE POL. Improved Distributed Algorithms for SCC Decomposition. Electronic Notes in Theoretical Computer Science. Elsevier, 2008, roč. 2008, 198(1), s. 63-77. ISSN 1571-0661.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla: ERCIM, 2008, s. 63-78. ISBN 978-3-642-03239-4.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Sven DRAŽAN a David ŠAFRÁNEK. Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE. In Electronic Notes in Theoretical Computer Science. Vol. 194/3. Elsevier: Elsevier Science, 2008, s. 35-50, 15 s. ISSN 1571-0661.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE-MC. 2008.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems. In QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems. Washington, DC, USA: IEEE Computer Society, 2008, s. 77-78. ISBN 978-0-7695-3360-5.

BARNAT, Jiří; Luboš BRIM; Pavel ŠIMEČEK a Michael WEBER. Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2008, s. 48-62. ISBN 978-3-540-78799-0.

BARNAT, Jiří a Petr ROČKAI. Shared Hash Tables in Parallel Model Checking. Electronic Notes in Theoretical Computer Science. Elsevier, 2008, roč. 2008, 198(1), s. 79-91, 12 s. ISSN 1571-0661.

BARNAT, Jiří a Luboš BRIM. Squeeze All the Power Out of Your Hardware to Verify Your Software! In Leveraging Applications of Formal Methods, Verification and Validation. Berlin Heidelberg: Springer, 2008, s. 604-618. ISBN 978-3-540-88478-1.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. DiVinE Multi-Core. 2007.

BARNAT, Jiří; Luboš BRIM a Pavel ŠIMEČEK. I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2007, s. 281-293. ISBN 978-3-540-73367-6.

BARNAT, Jiří a Pavel MORAVEC. Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In Formal Methods: Applications and Technology. Berlin, Heidelberg: Springer-Verlag, 2007, s. 316-330. ISBN 978-3-540-70951-0.

BARNAT, Jiri; Lubos BRIM a Martin LEUCKER. Parallel Model Checking and the FMICS-jETI Platform. In Proceedings Twelfth IEEE International Conference on Engineering of Complex Computer Systems. Los Alamitos: IEEE Computer Society, 2007, s. 330-339. ISBN 0-7695-2895-3.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE. 2007.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. ProbDiVinE: A Parallel Qualitative LTL Model Checker. In Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07). United States of America: IEEE Computer Society, 2007, s. 215-216. ISBN 0-7695-2883-X.

BARNAT, Jiří; Luboš BRIM a Petr ROČKAI. Scalable Multi-core LTL Model-Checking. In Model Checking Software. 1. vyd. Berlin, Heidelberg: Springer-Verlag, 2007, s. 187-203. ISBN 978-3-540-73369-0.

BRIM, Luboš a Jiří BARNAT. Tutorial: Parallel Model Checking. In Model Checking Software. Berlin, Heidelberg: Springer-Verlag, 2007, s. 2-3. ISBN 978-3-540-73369-0.

BARNAT, Jiří; Luboš BRIM a Ivana ČERNÁ. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin: Springer, 2006, s. 259-279. ISBN 978-3-540-36749-9.

BARNAT, Jiří a Ivana ČERNÁ. Distributed breadth-first search LTL model checking. Formal Methods in System Design. Springer Netherlands, 2006, roč. 29, č. 2, s. 117-134. ISSN 0925-9856.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Milan ČEŠKA a Jana TŮMOVÁ. Distributed Qualitative LTL Model Checking of Markov Decision Processes. In Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation. Bonn, Germany: University of Bonn, 2006, s. 1-15. ISSN 1571-0661.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Pavel MORAVEC; Petr ROČKAI a Pavel ŠIMEČEK. DiVinE -- A Tool for Distributed Verification. In Computer Aided Verification. Berlin: Springer Verlag, 2006, s. 278-281. ISBN 978-3-540-37406-0.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ; Pavel MORAVEC; Pavel ŠIMEČEK a Jakub CHALOUPKA. DiVinE Library. 2006.

BARNAT, Jiří a Pavel MORAVEC. Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In Proceedings of the 5th International Workshop on Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2006). Bonn, Germany: University Bonn, 2006, s. 20-34.

BARNAT, Jiří; Luboš BRIM a Ivana ČERNÁ. Distributed Analysis of Large Systems. In Formal Methods for Components and Objects. Amsterdam: CWI Amsterdam, 2005, s. 31-35, 4 s.

BARNAT, Jiří. Distributed Memory LTL Model Checking (Ph.D. Thesis). Brno: Masarykova Universita, 2005, 170 s. PhD Thesis.

BARNAT, Jiří; Luboš BRIM; Ivana ČERNÁ a Pavel ŠIMEČEK. DIVINE - The Distributed Verification Environment. In In proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisboa, Portugal: TU Munchen, 2005, s. 89-94.

BARNAT, Jiří; Vojtěch FOREJT; Martin LEUCKER a Michael WEBER. DivSPIN - A SPIN compatible distributed model checker. In Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC05). Lisabon, Portugalsko: TU Munchen, 2005, s. 95-100.

BARNAT, Jiří; Luboš BRIM a Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Electronical Notes in Theoretical Computer Science. Elsevier, 2005, roč. 2005, č. 133, s. 21-39, 10 s. ISSN 1571-0661.

BARNAT, Jiří; Luboš BRIM a Jakub CHALOUPKA. Distributed Memory LTL Model Checking Based on Breadth First Search. Brno: Faculty of Informatics, Masaryk University Brno, 2004, 57 s. FIMU-RS-2004-07.

BARNAT, Jiří; Luboš BRIM a Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. In Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2004). Linz, Austria: Institute for Systems Engineering & Automation, Kepler university Linz, 2004, s. 17-34. ISBN 3-902457-03-1.

BRIM, Luboš a Jiří BARNAT. Distribution of Explicit-State LTL Model-Checking. Editors Thomas Arts, Wan Fokking. Electronic Notes in Theoretical Computer Science. Elsevier Science, 2003, Volume 80, č. 1, s. 120-125.

BARNAT, Jiří; Luboš BRIM a Jakub CHALOUPKA. Parallel Breadth-First Search LTL Model-Checking. In 18th IEEE International Conference on Automated Software Engineering (ASE'03). Montreal: IEEE Computer Society, 2003, s. 106-115. ISBN 0-7695-2035-9.

BARNAT, Jiří. How to distribute LTL model-checking using decomposition of negative claim automaton. In SOFSEM 2002 Student Research Forum Proceedings. Milovy,Czech Republic: Slovak University of Technology, 2002, s. 9-14.

BARNAT, Jiří; Luboš BRIM a Ivana ČERNÁ. Property Driven Distribution of Nested DFS. In M. Leuschel and U. Ultes-Nitsche (Eds.): Proceedings of the 3rd International Workshop on Verification and Computational Logic. Pittsburgh, PA, USA: Dept. of Electronics and Computer Science, University of Southampton, 2002, s. 1-10.

BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. In F. Cassez, C. Jard, F. Laroussinie, and M.D. Ryan (Eds.): Modelling and Verification of Parallel processes. Nantes, France: IRCCyN, Ecole Centrale de Nantes, 2002, s. 262-267.

BARNAT, Jiří; Luboš BRIM a Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. In M.B. Dwyer (Ed.): Model Checking Software, 8th International SPIN Workshop. Toronto, Canada: Springer Verlag, 2001, s. 200-215. ISBN 3-540-42124-6.

BARNAT, Jiří; Luboš BRIM a Jitka STŘÍBRNÁ. Distributed LTL Model-Checking in SPIN. Brno: FI MU, 2000, 16 s. Technical Reports.