Curriculum Vitae

Curriculum vitae

Person Identification

• Jiří Barnat (11.3.1977-??)
  Married, 3 children (Klara, Magda, Tana).

Workplace

• Faculty of Informatics
  Botanicka 68a
  Brno
  602 00
  +420-549493507

Employment Position

• Professor

Education and Academic Qualifications

• Habilitation, Faculty of Informatics, MU, 2011
• PhD., Faculty of Informatics, MU Brno, 2005
• Master's degree, Faculty of Informatics, MU Brno, 2000

Employment Summary

• Professor, Faculty of Informatics (since January 2017)
• Associate Professor, Faculty of Informatics (since May 2011)
• Assistent Professor, Faculty of Informatics (since Feb 2005)
• External Teacher (4-6 hours/week), Faculty of Informatics (1999 - 2005)

Scientific and Research Interest

• Formal Verification (LTL Model-Checking, Probabilistic LTL)
• Parallel algorithms for inherently sequential problems
• Algorithm Engineering (multi-core performance tweaking, I/O efficient algorithms)
• Distributed robotic platforms

Academical Stays

• CWI, Amsterdam (1 month, 2007)
• University of Aalborg (3 months, 2005)
• INRIA Rhone-Alps (2 months, 2001)

University Activities

• Head of Parallel and Distributed Systems Laboratory (ParaDiSe)

Appreciation of Science Community

• Rector's award for being an excelent teacher (2015)
• Dean's award (2005)
• Dean's annual award (2000)

Selected Publications

• KEJSTOVÁ, Katarína, Petr ROČKAI and 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, p. 225-240. ISBN 978-3-319-67530-5. Available from: https://dx.doi.org/10.1007/978-3-319-67531-2_14. info
• BAUCH, Petr, Vojtěch HAVEL and Jiří BARNAT. Control Explicit-Data Symbolic Model Checking. ACM Transactions on Software Engineering and Methodology. 2016, vol. 25, No 2, p. 15-62. ISSN 1049-331X. Available from: https://dx.doi.org/10.1145/2888393. URL info
• ROČKAI, Petr, Jiří BARNAT and Luboš BRIM. Model checking C++ programs with exceptions. Science of Computer Programming. Elsevier B.V., 2016, vol. 128, 15 October 2016, p. 68-85. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2016.05.007. URL info
• Š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, 2016, p. 144-155. ISBN 978-3-319-29816-0. Available from: https://dx.doi.org/10.1007/978-3-319-29817-7_13. URL info
• MRÁZEK, Jan, Petr BAUCH, Henrich LAUKO and 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, p. 208-213. ISBN 978-3-319-32581-1. Available from: https://dx.doi.org/10.1007/978-3-319-32582-8_14. info
• 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, p. 46-57. ISBN 978-3-662-46077-1. Available from: https://dx.doi.org/10.1007/978-3-662-46078-8_5. http://dx.doi.org/10.1007/978-3-662-46078-8_5 info
• BARNAT, Jiří, Jan HAVLÍČEK and Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science, 2013, p. 79-93. ISSN 1571-0661. Available from: https://dx.doi.org/10.1016/j.entcs.2013.07.006. URL info
• BARNAT, Jiří, Luboš BRIM and 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, vol. 77, No 12, p. 1272-1288. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2011.03.001. URL info
• BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In NASA Formal Methods. Berlin: Springer-Verlag Berlin Heidelberg, 2012, p. 252-266. ISBN 978-3-642-28890-6. Available from: https://dx.doi.org/10.1007/978-3-642-28891-3_25. info
• BARNAT, Jiří, Luboš BRIM, Jan BERAN, Tomáš KRATOCHVÍLA and 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, p. 245-248. ISBN 978-0-7695-4751-0. info
• BARNAT, Jiří, Jan BERAN, Luboš BRIM, Tomáš KRATOCHVÍLA and 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, p. 78--92. ISBN 978-3-642-32468-0. Available from: https://dx.doi.org/10.1007/978-3-642-32469-7_6. info
• EDELKAMP, Stefan, Damian SULEWSKI, Jiří BARNAT, Luboš BRIM and Pavel ŠIMEČEK. Flash memory efficient LTL model checking. Science of Computer Programming. Elsevier, 2011, vol. 76, No 2, p. 136--157. ISSN 0167-6423. Available from: https://dx.doi.org/10.1016/j.scico.2010.03.005. URL info
• BARNAT, Jiří, Jakub CHALOUPKA and Jaco VAN DE POL. Distributed Algorithms for SCC Decomposition. Journal of Logic and Computation. Oxford University Press, 2011, vol. 21, No 1, p. 23-44. ISSN 0955-792X. Available from: https://dx.doi.org/10.1093/logcom/exp003. URL info
• BRIM, Luboš and Jiří BARNAT. Platform Dependent Verification: On Engineering Verification Tools for 21st Century. Electronic Proceedings in Theoretical Computer Science. 2011, vol. 72, No 2011, p. 1-12. ISSN 2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.72.1. EPTCS info
• BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA. Computing Optimal Cycle Mean in Parallel on CUDA. Electronic Proceedings in Theoretical Computer Science. 2011, vol. 72, No 2011, p. 68-83. ISSN 2075-2180. Available from: https://dx.doi.org/10.4204/EPTCS.72.8. EPTCS volume 72 info
• BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT). Springer-Verlag GmbH, 2010, vol. 12, No 2, p. 139-153. ISSN 1433-2779. Available from: https://dx.doi.org/10.1007/s10009-010-0136-z. URL info
• BARNAT, Jiří, Luboš BRIM and 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, p. 222-231. ISBN 978-0-7695-4153-2. info
• 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. Theoretical Computer Science. 2009, vol. 2009, No 410, p. 3128-3148, 20 pp. ISSN 0304-3975. URL info
• VERSTOEP, Kees, Henri E. BAL, Jiří BARNAT and Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE, 2009, p. 201-212. ISBN 978-1-4244-3751-1. info
• BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009, p. 53-68. ISBN 978-3-642-03239-4. Available from: https://dx.doi.org/10.1007/978-3-642-03240-0_8. URL info
• BARNAT, Jiří, Luboš BRIM, Stefan EDELKAMP, Damian SULEWSKI and Pavel ŠIMEČEK. Can Flash Memory Help in Model Checking? In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009, p. 150-165. ISBN 978-3-642-03239-4. Available from: https://dx.doi.org/10.1007/978-3-642-03240-0_14. URL info
• BARNAT, Jiří, Ivana ČERNÁ and 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, p. 21-30. ISBN 978-0-7695-3808-2. URL URL info
• BARNAT, Jiří, Luboš BRIM and Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science. 2009, vol. 14, Prosinec, p. 107--111. ISSN 2075-2180. URL info
• BARNAT, Jiří, Luboš BRIM, Milan ČEŠKA and Tomáš LAMR. CUDA Accelerated LTL Model Checking. In Proceedings of the 15th International Conference on Parallel and Distributed Systems. Neuveden: Roy Sterritt, 2009, p. 34-41. ISBN 978-0-7695-3900-3. info
• BARNAT, Jiří, Luboš BRIM and 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, p. 407-425. ISBN 978-3-642-10372-8. Available from: https://dx.doi.org/10.1007/978-3-642-10373-5_21. info
• BARNAT, Jiří, Luboš BRIM and 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, p. 635-639. ISBN 978-0-7695-3891-4. info
• BARNAT, Jiří, Jakub CHALOUPKA and Jaco VAN DE POL. Improved Distributed Algorithms for SCC Decomposition. Electronic Notes in Theoretical Computer Science. Elsevier, 2008, vol. 2008, 198(1), p. 63-77. ISSN 1571-0661. info
• BARNAT, Jiří and Petr ROČKAI. Shared Hash Tables in Parallel Model Checking. Electronic Notes in Theoretical Computer Science. Elsevier, 2008, vol. 2008, 198(1), p. 79-91, 12 pp. ISSN 1571-0661. info
• BARNAT, Jiří, Luboš BRIM, Pavel ŠIMEČEK and 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, p. 48-62. ISBN 978-3-540-78799-0. info
• BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. DiVinE Multi-Core -- A Parallel LTL Model-Checker. In Automated Technology for Verification and Analysis. Berlin / Heidelberg: Springer, 2008, p. 234-239. ISBN 978-3-540-88386-9. info
• BARNAT, Jiří and Pavel MORAVEC. Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In Formal Methods: Applications and Technology. Berlin, Heidelberg: Springer-Verlag, 2007, p. 316-330. ISBN 978-3-540-70951-0. info
• BARNAT, Jiří, Luboš BRIM and Pavel ŠIMEČEK. I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2007, p. 281-293. ISBN 978-3-540-73367-6. info
• BRIM, Luboš and Jiří BARNAT. Tutorial: Parallel Model Checking. In Model Checking Software. Berlin, Heidelberg: Springer-Verlag, 2007, p. 2-3. ISBN 978-3-540-73369-0. info
• BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Scalable Multi-core LTL Model-Checking. In Model Checking Software. 1st ed. Berlin, Heidelberg: Springer-Verlag, 2007, p. 187-203. ISBN 978-3-540-73369-0. info
• BARNAT, Jiri, Lubos BRIM and 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, p. 330-339. ISBN 0-7695-2895-3. info
• BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and 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, p. 215-216. ISBN 0-7695-2883-X. info
• BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Pavel MORAVEC, Petr ROČKAI and Pavel ŠIMEČEK. DiVinE -- A Tool for Distributed Verification. In Computer Aided Verification. Berlin: Springer Verlag, 2006, p. 278-281. ISBN 978-3-540-37406-0. info
• BARNAT, Jiří and 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, p. 20-34. info
• BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and 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, p. 1-15. ISSN 1571-0661. info
• BARNAT, Jiří, Luboš BRIM and Ivana ČERNÁ. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin: Springer, 2006, p. 259-279. ISBN 978-3-540-36749-9. info
• BARNAT, Jiří and Ivana ČERNÁ. Distributed breadth-first search LTL model checking. Formal Methods in System Design. Springer Netherlands, 2006, vol. 29, No 2, p. 117-134. ISSN 0925-9856. URL info
• BARNAT, Jiří, Luboš BRIM and Ivana ČERNÁ. Distributed Analysis of Large Systems. In Formal Methods for Components and Objects. Amsterdam: CWI Amsterdam, 2005, p. 31-35, 4 pp. info
• BARNAT, Jiří, Vojtěch FOREJT, Martin LEUCKER and 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, p. 95-100. info
• BARNAT, Jiří. Distributed Memory LTL Model Checking (Ph.D. Thesis). Brno: Masarykova Universita, 2005, 170 pp. PhD Thesis. info
• BARNAT, Jiří, Luboš BRIM and 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, p. 17-34. ISBN 3-902457-03-1. info
• BARNAT, Jiří, Luboš BRIM and Jakub CHALOUPKA. Distributed Memory LTL Model Checking Based on Breadth First Search. Brno: Faculty of Informatics, Masaryk University Brno, 2004, 57 pp. FIMU-RS-2004-07. URL info
• BARNAT, Jiří, Luboš BRIM and 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, p. 1-10. info
• 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, p. 262-267. info
• BARNAT, Jiří, Luboš BRIM and 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, p. 200-215. ISBN 3-540-42124-6. info
• BARNAT, Jiří. Verifikace souběžných procesů s použitím nástroje SPIN. Brno, 2000, 62 s. info

2018/09/06