To pronounce my surname correctly, read "stray czech". Professor at Faculty of Informatics, Masaryk University, Brno. Member of the Laboratory of Formal Methods, Logic and Algorithms (Formela). Contact Faculty of Informatics Masaryk University Botanická 68a 602 00 Brno, Czech Republic Office: C414 Phone: +420-549 49 69 41 Email: strejcek@fi.muni.cz Consultations:   on request Research Publications DBLP Google Scholar ORCID 0000-0001-5873-403X Tools ClabureDB - Classified bug-reports database HOAF - Hanoi omega-automata format LTL3BA - Translator of LTL to Büchi automata LTL3DRA - Translator of an LTL fragment to deterministic Rabin automata LTL3TELA - Translator of LTL to nondeterministic Emerson-Lei automata Q3B - SMT solver for quantified bit-vector theory Seminator - Tool for semi-determinization of nondeterministic automata Symbiotic - Program analysis tool based on instrumentation, slicing, and symbolic execution Research interests Automata over infinite words: translation from LTL, reduction, transformation, and applications Automatic analysis and verification of software and hardware systems SMT-solving, focused on bit-vector logic PhD students Current Paulína Ayaziová Vincent Mihalkovič Juraj Major (suspended) Completed Marek Chalupa - Program Slicing and Symbolic Execution for Verification (2022) Martin Jonáš - Satisfiability of Quantified Bit-Vector Formulas: Theory and Practice (2019) František (Fanda) Blahoudek - Automata for Formal Methods: Little Steps Towards Perfection (2018) Tomáš Babiak - Translation of Linear Temporal Logic to Omega-Automata (2017, as consultant) Jiří Slabý - Automatic Bug-finding Techniques for Large Software Projects (2014, as consultant) Marek Trtík - Symbolic Execution and Program Loops (2014, as consultant) Teaching Autumn semesters IB107 - Computability and Complexity, 2020-now IA159 - Formal Methods for Software Analysis, 2023-now IA072 - Seminar on Verification, 2019-now Spring semesters IA169 - Model Checking, 2024-now IA072 - Seminar on Verification, 2020-now Past courses IB102 - Automata and Grammars, 2006-2012, 2017-2019 IB102 - Automata, Grammars, and Complexity, 2013-2016 IA159 - Formal Verification Methods, 2008-2012, 2014-2023 IB112 - Math Foundations, 2010-2012, 2014-2019 IA072 - Seminar on Concurrency, 2008-2019 DUCIT - Teaching lab, 2022 IB005 - Formal Languages and Automata I (seminar tutor), 2007-2012, 2014-2023 IA008 - Computational Logic (in Czech) (seminar tutor), 2007-2009 IA006 - Selected Topics on Automata Theory (seminar tutor), 2008-2023 IB002 - Design of Algorithms I (seminar tutor), 2008 IB107 - Computability and Complexity (seminar tutor), 2003, 2004, 2006 I007 - Computability (seminar tutor), 1998-2003 strejcek@fi.muni.cz