To pronounce my surname correctly, read "stray czech". Associate 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 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 Marek Chalupa Juraj Major (suspended) Jiří Zárevúcky (formal supervision, in practice supervised by Petr Novotný) Completed 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 IA072 - Seminar on Verification, 2020-now IA006 - Selected Topics on Automata Theory (seminar tutor), 2008-now Spring semesters IA159 - Formal Verification Methods, 2008-2012, 2014-now IA072 - Seminar on Verification, 2019-now IB005 - Formal Languages and Automata I (seminar tutor), 2007-2012, 2014-now Past courses IB102 - Automata and Grammars, 2006-2012, 2017-2019 IB102 - Automata, Grammars, and Complexity, 2013-2016 IB112 - Math Foundations, 2010-2012, 2014-2019 IA072 - Seminar on Concurrency, 2008-2019 IA008 - Computational Logic (in Czech) (seminar tutor), 2007-2009 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