prof. RNDr. Jiří Barnat, Ph.D.

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 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://dx.doi.org/10.1007/978-3-319-67531-2_14. info
• 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://dx.doi.org/10.1145/2888393. URL info
• 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://dx.doi.org/10.1016/j.scico.2016.05.007. URL info
• Š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://dx.doi.org/10.1007/978-3-319-29817-7_13. URL info
• 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://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, s. 46-57. ISBN 978-3-662-46077-1. Dostupné z: 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 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://dx.doi.org/10.1016/j.entcs.2013.07.006. URL info
• 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://dx.doi.org/10.1016/j.scico.2011.03.001. URL info
• 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://dx.doi.org/10.1007/978-3-642-28891-3_25. info
• 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. info
• 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://dx.doi.org/10.1007/978-3-642-32469-7_6. info
• 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://dx.doi.org/10.1016/j.scico.2010.03.005. URL info
• 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://dx.doi.org/10.1093/logcom/exp003. URL info
• 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://dx.doi.org/10.4204/EPTCS.72.1. EPTCS info
• 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://dx.doi.org/10.4204/EPTCS.72.8. EPTCS volume 72 info
• 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://dx.doi.org/10.1007/s10009-010-0136-z. URL info
• 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. info
• 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. URL info
• 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. info
• 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://dx.doi.org/10.1007/978-3-642-03240-0_8. URL info
• 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://dx.doi.org/10.1007/978-3-642-03240-0_14. URL info
• 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. URL URL info
• 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. URL info
• 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. info
• 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://dx.doi.org/10.1007/978-3-642-10373-5_21. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. info
• 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. URL info
• 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. info
• 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. info
• BARNAT, Jiří. Distributed Memory LTL Model Checking (Ph.D. Thesis). Brno: Masarykova Universita, 2005, 170 s. PhD Thesis. info
• 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. info
• 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. URL info
• 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. 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, s. 262-267. info
• 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. info
• BARNAT, Jiří. Verifikace souběžných procesů s použitím nástroje SPIN. Brno, 2000, 62 s. info

2018/09/06