• Skip the Organizational structure panel
• Organizational structure

  On selecting a constituent part of MU the "Staff" page will be displayed with information relevant to the selected constituent part. The "Staff" page is not available for non-activated items.

  Masaryk University

  • Faculties
  • Law
  • Medicine
  • Science
  • Arts
  • Education
  • Economics
  • Informatics
  • Social Studies
  • Sports Studies

  • Institutes
  • Computer Science
  • CEITEC MU
  • Politica
  • Specialized Units
  • Hostels & Canteens
  • University Press
  • Telč Centre
  • UCB Management

  • Rector`s Office
  • Rectorate
  • Other Units
  • Archive
  • Language Centre
  • International Studies
  • Disabled Students
  • Technology Transfer
  • Biostatistics
  • Mendel Museum
  • CERIT
  • Civic Education
  • Project Team CEITEC

   

Assoc. Prof. RNDr. Jiří Barnat, Ph.D.

 

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

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

• Assistant Professor

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

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

• Parallel algorithms for inherently sequential problems
• Formal Verification (LTL Model-Checking, Probabilistic LTL)
• Algorithm Engineering (multi-core performance tweaking, I/O efficient algorithms)
• Systems Biology (Simulation of Gene Regulatory Networks)

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

• Member of Parallel and Distributed Systems Laboratory (ParaDiSe)

• Dean's award (2005)
• Dean's annual award (2000)

• BARNAT, Jiří a 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, 2011. ISSN 0167-6423. 2012. URL info
• BARNAT, Jiří a Luboš BRIM a Petr ROČKAI. Towards LTL Model Checking of Unmodified Thread-Based C & C++ Programs. In NASA Formal Methods. : Springer-Verlag Berlin Heidelberg, 2012. od s. 252-266, 15 s. ISBN 978-3-642-28890-6.  info
• EDELKAMP, Stefan a Damian SULEWSKI a Jiří BARNAT a Luboš BRIM a Pavel ŠIMEČEK. Flash memory efficient LTL model checking. Science of Computer Programming, Elsevier, 76, 2, od s. 136--157, 22 s. ISSN 0167-6423. 2011. doi:10.1016/j.scico.2010.03.005. URL info
• BARNAT, Jiří a Jakub CHALOUPKA a Jaco VAN DE POL. Distributed Algorithms for SCC Decomposition. Journal of Logic and Computation, Oxford University Press, 21, 1, od s. 23-44, 22 s. ISSN 0955-792X. 2011. doi: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, 72, 2011, od s. 1-12, 12 s. ISSN 2075-2180. 2011. doi:10.4204/EPTCS.72.1. EPTCS info
• BARNAT, Jiří a Petr BAUCH a Luboš BRIM a Milan ČEŠKA. Computing Optimal Cycle Mean in Parallel on CUDA. Electronic Proceedings in Theoretical Computer Science, 72, 2011, od s. 68-83, 16 s. ISSN 2075-2180. 2011. doi:10.4204/EPTCS.72.8. EPTCS volume 72 info
• BARNAT, Jiří a Luboš BRIM a Petr ROČKAI. Scalable shared memory LTL model checking. International Journal on Software Tools for Technology Transfer (STTT), Springer-Verlag GmbH, 12, 2, od s. 139-153, 15 s. ISSN 1433-2779. 2010. URL info
• BARNAT, Jiří a 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. od s. 222-231, 10 s. ISBN 978-0-7695-4153-2.  info
• BARNAT, Jiří a Luboš BRIM a Ivana ČERNÁ a Sven DRAŽAN a Jana FABRIKOVÁ a David ŠAFRÁNEK. On Algorithmic Analysis of Transcriptional Regulation by LTL Model Checking. Theoretical Computer Science, 2009, 410, od s. 3128-3148, 20 s. ISSN 0304-3975. 2009. URL info
• VERSTOEP, Kees a Henri E. BAL a Jiří BARNAT a Luboš BRIM. Efficient Large-Scale Model Checking. In 23rd IEEE International Parallel & Distributed Processing Symposium. IEEE: IEEE, 2009. od s. 201-212, 12 s. ISBN 978-1-4244-3751-1.  info
• BARNAT, Jiří a Luboš BRIM a Ivana ČERNÁ a Milan ČEŠKA a Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In Formal Methods for Industrial Critical Systems. Neuveden: Springer Berlin / Heidelberg, 2009. od s. 53-68, 16 s. ISBN 978-3-642-03239-4. URL info
• BARNAT, Jiří a Luboš BRIM a Stefan EDELKAMP a 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. od s. 150-165, 16 s. ISBN 978-3-642-03239-4. URL info
• BARNAT, Jiří a 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. od s. 21-30, 10 s. ISBN 978-0-7695-3808-2. URL info
• BARNAT, Jiří a Luboš BRIM a Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science, 14, Prosinec, od s. 107--111, 5 s. ISSN 2075-2180. 2009. URL info
• BARNAT, Jiří a Luboš BRIM a 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. od s. 34-41, 8 s. ISBN 978-0-7695-3900-3.  info
• BARNAT, Jiří a 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. od s. 407-425, 19 s. ISBN 978-3-642-10372-8.  info
• BARNAT, Jiří a 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. od s. 635-639, 5 s. ISBN 978-0-7695-3891-4.  info
• BARNAT, Jiří a Jakub CHALOUPKA a Jaco VAN DE POL. Improved Distributed Algorithms for SCC Decomposition. Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 198(1), od s. 63-77, 15 s. ISSN 1571-0661. 2008.  info
• BARNAT, Jiří a Petr ROČKAI. Shared Hash Tables in Parallel Model Checking. Electronic Notes in Theoretical Computer Science, Elsevier, 2008, 198(1), od s. 79-91, 12 s. ISSN 1571-0661. 2008.  info
• BARNAT, Jiří a Luboš BRIM a 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. od s. 48-62, 15 s. ISBN 978-3-540-78799-0.  info
• BARNAT, Jiří a 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. od s. 234-239, 6 s. 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. od s. 316-330, 15 s. ISBN 978-3-540-70951-0.  info
• BARNAT, Jiří a Luboš BRIM a Pavel ŠIMEČEK. I/O Efficient Accepting Cycle Detection. In 19th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2007. od s. 281-293, 13 s. 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. od s. 2-3, 2 s. ISBN 978-3-540-73369-0.  info
• BARNAT, Jiří a Luboš BRIM a Petr ROČKAI. Scalable Multi-core LTL Model-Checking. In Model Checking Software. 1. vyd. Berlin, Heidelberg: Springer-Verlag, 2007. od s. 187-203, 17 s. ISBN 978-3-540-73369-0.  info
• BARNAT, Jiri a 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. od s. 330-339, 10 s. ISBN 0-7695-2895-3.  info
• BARNAT, Jiří a Luboš BRIM a Ivana ČERNÁ a 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. od s. 215-216, 2 s. ISBN 0-7695-2883-X.  info
• BARNAT, Jiří a Luboš BRIM a Ivana ČERNÁ a Pavel MORAVEC a Petr ROČKAI a Pavel ŠIMEČEK. DiVinE -- A Tool for Distributed Verification. In Computer Aided Verification. Berlin: Springer Verlag, 2006. od s. 278-281, 4 s. 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ří a Luboš BRIM a Ivana ČERNÁ a 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ří a Luboš BRIM a Ivana ČERNÁ. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin: Springer, 2006. od s. 259-279, 21 s. 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, 29, 2, od s. 117-134, 18 s. ISSN 0925-9856. 2006. URL info
• BARNAT, Jiří a Luboš BRIM a Ivana ČERNÁ. Distributed Analysis of Large Systems. In Formal Methods for Components and Objects. Amsterdam: CWI Amsterdam, 2005. od s. 31-35, 4 s.  info
• BARNAT, Jiří a Vojtěch FOREJT a 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. od s. 95-100, 6 s.  info
• BARNAT, Jiří. Distributed Memory LTL Model Checking (Ph.D. Thesis). Brno: Masarykova Universita, 2005. 170 s. PhD Thesis.  info
• BARNAT, Jiří a 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. od s. 17-34, 18 s. ISBN 3-902457-03-1.  info
• BARNAT, Jiří a 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ří a 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ří a 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. + di.  info

Last update: 2010/05/27