Publication Records

MRÁZEK, Jan, Vladimír CHLUP and 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. p. 1-8. ISBN 979-8-3503-2069-5. Available from: https://dx.doi.org/10.1109/CASE56687.2023.10260364

MRÁZEK, Jan and 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. p. 1-8. ISBN 979-8-3503-2069-5. Available from: https://dx.doi.org/10.1109/CASE56687.2023.10260586

MRÁZEK, Jan, Patrick ONDIKA, Ivana ČERNÁ and 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. p. 11894-11900. ISBN 979-8-3503-2365-8. Available from: https://dx.doi.org/10.1109/ICRA48891.2023.10160352

ROČKAI, Petr and Jiří BARNAT. DivSIM , an interactive simulator for LLVM bitcode. Online. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. GERMANY: SPRINGER HEIDELBERG, vol. 24, No 3, p. 493-510. ISSN 1433-2779. Available from: https://dx.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Á and Tadeáš KUČERA. DIVINE 4.4. Online

MRÁZEK, Jan, Martin JONÁŠ and 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. p. 6935-6940. ISBN 978-1-6654-1714-3. Available from: https://dx.doi.org/10.1109/IROS51168.2021.9636534

ROČKAI, Petr, Zuzana BARANOVÁ, Jan MRÁZEK, Katarína KEJSTOVÁ and Jiří BARNAT. Reproducible execution of POSIX programs with DiOS. Online. Software & Systems Modeling. Springer, vol. 20, No 2, p. 363-382. ISSN 1619-1366. Available from: https://dx.doi.org/10.1007/s10270-020-00837-y

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

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

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

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

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

MRÁZEK, Jan and Jiří BARNAT. RoFICoM - First Open-Hardware Connector for Metamorphic Robots. Online. In 2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). Neuveden: IEEE. p. 2720-2725. ISBN 978-1-72814-004-9. Available from: https://dx.doi.org/10.1109/IROS40897.2019.8968167

ROČKAI, Petr, Vladimír ŠTILL, Ivana ČERNÁ and Jiří BARNAT. DiVM: Model checking with LLVM and graph memory. Online. Journal of Systems and Software. Elsevier, vol. 143, Oct, p. 1-13. ISSN 0164-1212. Available from: https://dx.doi.org/10.1016/j.jss.2018.04.026

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

BEZDĚK, Peter, Nikola BENEŠ, Ivana ČERNÁ and Jiří BARNAT. On clock-aware LTL parameter synthesis of timed automata. Online. Journal of Logical and Algebraic Methods in Programming. ELSEVIER SCIENCE INC, 360 PARK AVE SOUTH: Elsevier, vol. 99, Oct, p. 114-142. ISSN 2352-2208. Available from: https://dx.doi.org/10.1016/j.jlamp.2018.05.004

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

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

KEJSTOVÁ, Katarína, Petr ROČKAI and Jiří BARNAT. From Model Checking to Runtime Verification and Back. Online. In Shuvendu Lahiri, Giles Reger. Runtime Verification - 17th International Conference, RV 2017. neuvedeno: Springer. p. 225-240. ISBN 978-3-319-67530-5. Available from: https://dx.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 and Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. Online. In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Cham: Springer International Publishing. p. 201-207. ISBN 978-3-319-68166-5. Available from: https://dx.doi.org/10.1007/978-3-319-68167-2_14

MRÁZEK, Jan, Martin JONÁŠ, Vladimír ŠTILL, Henrich LAUKO and Jiří BARNAT. Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution). Online. 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. p. 390-393. ISBN 978-3-662-54579-9. Available from: https://dx.doi.org/10.1007/978-3-662-54580-5_29

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

ŠTILL, Vladimír, Petr ROČKAI and 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. p. 54-64. ISBN 978-1-5386-0592-9. Available from: https://dx.doi.org/10.1109/QRS.2017.15

BAUCH, Petr, Vojtěch HAVEL and Jiří BARNAT. Accelerating Temporal Verification of Simulink Diagrams Using Satisfiability Modulo Theories. Online. Software Quality Journal. Springer, vol. 24, No 1, p. 37-63. ISSN 0963-9314. Available from: https://dx.doi.org/10.1007/s11219-014-9259-x

BARNAT, Jiří, Petr BAUCH, Nikola BENEŠ, Luboš BRIM, Jan BERAN and Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. Online. Formal Aspects of Computing. vol. 28, No 1, p. 45-63. ISSN 0934-5043. Available from: https://dx.doi.org/10.1007/s00165-015-0348-9

BAUCH, Petr, Vojtěch HAVEL and Jiří BARNAT. Control Explicit-Data Symbolic Model Checking. Online. ACM Transactions on Software Engineering and Methodology. vol. 25, No 2, p. 15-62. ISSN 1049-331X. Available from: https://dx.doi.org/10.1145/2888393

ŠTILL, Vladimír, Petr ROČKAI and Jiří BARNAT. DIVINE: Explicit-State LTL Model Checker. Online. 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. p. 920-922. ISBN 978-3-662-49673-2. Available from: https://dx.doi.org/10.1007/978-3-662-49674-9_60

BENDÍK, Jaroslav, Nikola BENEŠ, Jiří BARNAT and Ivana ČERNÁ. Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis (Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis). Online. 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. p. 121-136. ISBN 978-3-319-41590-1. Available from: https://dx.doi.org/10.1007/978-3-319-41591-8_9

BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT and Ivana ČERNÁ. LTL Parameter Synthesis of Parametric Timed Automata. Online. 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. p. 172-187. ISBN 978-3-319-41590-1. Available from: https://dx.doi.org/10.1007/978-3-319-41591-8_12

ROČKAI, Petr, Jiří BARNAT and Luboš BRIM. Model checking C++ programs with exceptions. Online. Science of Computer Programming. Elsevier B.V., vol. 128, 15 October 2016, p. 68-85. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2016.05.007

BARNAT, Jiří, Ivana ČERNÁ, Petr ROČKAI, Vladimír ŠTILL and Kristína ZÁKOPČANOVÁ. On verifying C++ programs with probabilities (On verifying {C++} programs with probabilities). Online. In Sascha Ossowski. Proceedings of the 31st Annual ACM Symposium on Applied Computing. Pisa: ACM New York, NY, USA. p. 1238-1243. ISBN 978-1-4503-3739-7. Available from: https://dx.doi.org/10.1145/2851613.2851721

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

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

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

ŠTILL, Vladimír, Petr ROČKAI and 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. p. 144-155. ISBN 978-3-319-29816-0. Available from: https://dx.doi.org/10.1007/978-3-319-29817-7_13

BARNAT, Jiří, Petr ROČKAI, Vladimír ŠTILL and Jiří WEISER. Fast, Dynamically-Sized Concurrent Hash Table. Online. In Bernd Fischer, Jaco Geldenhuys. Model Checking Software. Neuveden: Springer International Publishing. p. 49-65. ISBN 978-3-319-23403-8. Available from: https://dx.doi.org/10.1007/978-3-319-23404-5_5

BARNAT, Jiří. Quo Vadis Explicit-State Model Checking. Online. 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. p. 46-57. ISBN 978-3-662-46077-1. Available from: https://dx.doi.org/10.1007/978-3-662-46078-8_5

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

ŠTILL, Vladimír, Petr ROČKAI and Jiří BARNAT. Context-Switch-Directed Verification in DIVINE. Online. 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. p. 135-146. ISBN 978-3-319-14895-3. Available from: https://dx.doi.org/10.1007/978-3-319-14896-0_12

BAUCH, Petr, Vojtěch HAVEL and Jiří BARNAT. LTL Model Checking of LLVM Bitcode with Symbolic Data. Online. In P. Hlineny et al. Proceedings of MEMICS'14. Telc: Springer. p. 47-59. ISBN 978-3-319-14895-3. Available from: https://dx.doi.org/10.1007/978-3-319-14896-0_5

BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT and Ivana ČERNÁ. LTL Model Checking of Parametric Timed Automata. Online. 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. p. 28-39. ISBN 978-80-214-5022-6

ROČKAI, Petr, Jiří BARNAT and Luboš BRIM. Model Checking C++ with Exceptions. Online. Electronic Communications of the EASST. vol. 70, Listopad, p. 1-15. ISSN 1863-2122. Available from: https://dx.doi.org/10.14279/tuj.eceasst.70.983

BARNAT, Jiří, Petr BAUCH and 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. p. 756-759. ISSN 1066-6192. Available from: https://dx.doi.org/10.1109/PDP.2014.44

BEZDĚK, Peter, Nikola BENEŠ, Vojtěch HAVEL, Jiří BARNAT and Ivana ČERNÁ. On Clock-Aware LTL Properties of Timed Automata. Online. In Gabriel Ciobanu, Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014. Neuveden: Springer International Publishing. p. 43-60. ISBN 978-3-319-10881-0. Available from: https://dx.doi.org/10.1007/978-3-319-10882-7_4

BARNAT, Jiří, Petr BAUCH and Vojtěch HAVEL. Temporal Verification of Simulink Diagrams. Online. In P. J. Clarke et al. Proceedings of HASE 2014. Miami: IEEE Computer Society. p. 81-88. ISBN 978-1-4799-3465-2. Available from: https://dx.doi.org/10.1109/HASE.2014.20

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

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

BARNAT, Jiří, Jan HAVLÍČEK and Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. Online. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science. p. 79-93. ISSN 1571-0661. Available from: https://dx.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 and Jan KRIHO. DIVINE 3.0. Online

BARNAT, Jiří, 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. Online. In Sharygina, Natasha; Veith, Helmut. Computer Aided Verification 2013. Heidelberg: Springer. p. 863-868. ISBN 978-3-642-39798-1. Available from: https://dx.doi.org/10.1007/978-3-642-39799-8_60

YORDANOV, Boyan, Jana TŮMOVÁ, Ivana ČERNÁ, Jiří BARNAT and Calin BELTA. Formal analysis of piecewise affine systems through formula-guided refinement. Online. Automatica. Elsevier, vol. 49, No 1, p. 261-266. ISSN 0005-1098. Available from: https://dx.doi.org/10.1016/j.automatica.2012.09.027

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

BARNAT, Jiří, Luboš BRIM and Vojtěch HAVEL. LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model. Online. In Juan E. Guerrero. Proceedings of Application of Concurrency to System Design, 2013. Barcelona: IEEE Computer Society. p. 51-59. ISBN 978-0-7695-5035-0. Available from: https://dx.doi.org/10.1109/ACSD.2013.8

SVOREŇOVÁ, Mária, Jana TŮMOVÁ, Jiří BARNAT and 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. p. 6749-6754. ISBN 978-1-4673-2066-5. Available from: https://dx.doi.org/10.1109/CDC.2012.6426041

BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA. Designing Fast LTL Model Checking Algorithms for Many-core GPUs. Online. Journal of Parallel and Distributed Computing. Elsevier, vol. 72, No 9, p. 1083-1097. ISSN 0743-7315. Available from: https://dx.doi.org/10.1016/j.jpdc.2011.10.015

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

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

BARNAT, Jiří, Luboš BRIM, Adam KREJČÍ, Adam STRECK, David ŠAFRÁNEK, Martin VEJNÁR and Tomáš VEJPUSTEK. On Parameter Synthesis by Parallel Model Checking. Online. IEEE/ACM Transactions on Computational Biology and Bioinformatics. Los Alamitos: IEEE Computer Society, vol. 9, No 3, p. 693-705. ISSN 1545-5963. Available from: https://dx.doi.org/10.1109/TCBB.2011.110

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Online. Science of Computer Programming. Elsevier, vol. 77, No 12, p. 1272-1288. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2011.03.001

YORDANOV, Boyan, Jana TŮMOVÁ, Ivana ČERNÁ, Jiří BARNAT and Calin BELTA. Temporal Logic Control of Discrete-Time Piecewise Affine Systems. Online. IEEE Transactions on Automatic Control. PISCATAWAY, vol. 57, No 6, p. 1491-1504. ISSN 0018-9286. Available from: https://dx.doi.org/10.1109/TAC.2011.2178328

BARNAT, Jiří, Ivana ČERNÁ and Jana TŮMOVÁ. Timed Automata Approach to Verification of Systems with Degradation. Online. In MEMICS 2011. LNCS 7119. Heidelberg: Springer. p. 84 - 93. ISBN 978-3-642-25928-9. Available from: https://dx.doi.org/10.1007/978-3-642-25929-6_8

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

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. Online. In NASA Formal Methods. Berlin: Springer-Verlag Berlin Heidelberg. p. 252-266. ISBN 978-3-642-28890-6. Available from: https://dx.doi.org/10.1007/978-3-642-28891-3_25

BARNAT, Jiří, Ivana ČERNÁ and Jana TŮMOVÁ. Verification of Systems with Degradation. Online. Computing and Informatics. vol. 31, No 3, p. 507-530. ISSN 1335-9150

BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA. Computing Optimal Cycle Mean in Parallel on CUDA. Online. Electronic Proceedings in Theoretical Computer Science. vol. 72, No 2011, p. 68-83. ISSN 2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.72.8

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

BARNAT, Jiří, Jakub CHALOUPKA and Jaco VAN DE POL. Distributed Algorithms for SCC Decomposition. Online. Journal of Logic and Computation. Oxford University Press, vol. 21, No 1, p. 23-44. ISSN 0955-792X. Available from: https://dx.doi.org/10.1093/logcom/exp003

EDELKAMP, Stefan, Damian SULEWSKI, Jiří BARNAT, Luboš BRIM and Pavel ŠIMEČEK. Flash memory efficient LTL model checking. Online. Science of Computer Programming. Elsevier, vol. 76, No 2, p. 136--157. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2010.03.005

BRIM, Luboš and Jiří BARNAT. Platform Dependent Verification: On Engineering Verification Tools for 21st Century. Online. Electronic Proceedings in Theoretical Computer Science. vol. 72, No 2011, p. 1-12. ISSN 2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.72.1

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

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

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. DiVinE 2.4. Online

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

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

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

BARNAT, Jiří, Luboš BRIM, Petr BAUCH and Milan ČEŠKA. MWC-DiVinE. Online

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

BARNAT, Jiří, Luboš BRIM, David ŠAFRÁNEK and Martin VEJNÁR. Parameter Scanning by Parallel Model Checking with Applications in Systems Biology. Online. 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. p. 95-104. ISBN 978-0-7695-4265-2

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

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Scalable shared memory LTL model checking. Online. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, vol. 12, No 2, p. 139-153. ISSN 1433-2779. Available from: https://dx.doi.org/10.1007/s10009-010-0136-z

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. Online. In Formal Methods and Software Engineering. Germany: Springer Berlin / Heidelberg. p. 407-425. ISBN 978-3-642-10372-8. Available from: https://dx.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 and Ma HONGWU. BioDiVinE: A Framework for Parallel Analysis of Biological Models. Online. In Proceedings of 2nd International Workshop on Computational Models for Cell Processes. Neuveden: EPTCS. p. 31-45. ISSN 2075-2180

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

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

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

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

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

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

ROČKAI, Petr, Jiří BARNAT, Luboš BRIM and Milan ČEŠKA. DiVinE 2.0. Online

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

BARNAT, Jiří, Luboš BRIM and Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Online. Electronic Proceedings in Theoretical Computer Science. vol. 14, Prosinec, p. 107--111. ISSN 2075-2180

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

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

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

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

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

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

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

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

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

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

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

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

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

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

BARNAT, Jiří and Petr ROČKAI. Shared Hash Tables in Parallel Model Checking. Online. Electronic Notes in Theoretical Computer Science. Elsevier, vol. 2008, 198(1), p. 79-91, 12 pp. ISSN 1571-0661

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

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. DiVinE Multi-Core. Online

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

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

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

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

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

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Scalable Multi-core LTL Model-Checking. Online. In Model Checking Software. 1st ed. Berlin, Heidelberg: Springer-Verlag. p. 187-203. ISBN 978-3-540-73369-0

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

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

BARNAT, Jiří and Ivana ČERNÁ. Distributed breadth-first search LTL model checking. Online. Formal Methods in System Design. Springer Netherlands, vol. 29, No 2, p. 117-134. ISSN 0925-9856

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

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

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

BARNAT, Jiří and Pavel MORAVEC. Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. Online. 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. p. 20-34

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

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

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

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

BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Online. Electronical Notes in Theoretical Computer Science. Elsevier, vol. 2005, No 133, p. 21-39, 10 pp. ISSN 1571-0661

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

BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. From Distributed Memory Cycle Detection to Parallel LTL Model Checking. Online. 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. p. 17-34. ISBN 3-902457-03-1

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

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

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

BARNAT, Jiří, Luboš BRIM and Ivana ČERNÁ. Property Driven Distribution of Nested DFS. Online. 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. p. 1-10

BARNAT, Jiří. Using verified property to partition the state space in LTL model-checking. Online. 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. p. 262-267

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

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