prof. RNDr. Jan Strejček, Ph.D.

Curriculum vitae

Person Identification

• Jan Strejček, born 21 May, 1977 in Brno, Czechoslovakia. Married.

Workplace

• Department of Computer Science
  Faculty of Informatics
  Masaryk University
  Botanická 68a
  602 00 Brno
  Czech Republic

Employment Position

• Professor

Education and Academic Qualifications

• 2022: Professor in Informatics, Masaryk University, Brno, Czech Republic.
• 2013: Doc. (habilitation) in Informatics, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2007: RNDr. in Informatics, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2005: Ph.D. in Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic. Thesis: Linear Temporal Logic: Expressiveness and Model Checking. Supervisor: Mojmír Křetínský.
• 2001: Mgr. (master's degree) in Informatics, Faculty of Informatics, Masaryk University, Brno, Czech Republic. Thesis: Models of Infinite-State Systems with Constraints. Supervisor: Antonín Kučera.
• 2000: Mgr. (master's degree) in Mathematics, Faculty of Science, Masaryk University, Brno, Czech Republic. Thesis: Constrained Rewrite Transition Systems. Supervisor: Luboš Brim.

Employment Summary

• 2023-now: Professor, Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2013-2022: Associate professor, Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2006-2013: Assistant professor, Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2005-2006: Post-doc researcher, LaBRI, University of Bordeaux 1, France (12 months).
• 2005: Assistant professor, Department of Computer Science, Faculty of Informatics, Masaryk University, Brno, Czech Republic.

Pedagogical Activities

• 2023-now: Formal Methods for Software Analysis
• 2020-now: Computability and Complexity
• 2019-now: Seminar on Verification
• 2010-2012, 2014-2019: Math Foundations
• 2008-2023: Formal Verification Methods
• 2008-2019: Seminar on Concurrency
• 2006-2012, 2017-2019: Automata and Grammars
• 2013-2016: Automata, Grammars, and Complexity
• 2008-2023: Selected Topics on Automata Theory (seminar tutor)
• 2007-2023: Formal Languages and Automata I (seminar tutor)
• 2008: Design of Algorithms I (seminar tutor)
• 2007-2009: Computational Logic (seminar tutor)
• 2003-2004, 2006: Computability and Complexity (seminar tutor)
• 1998-2002: Computability (seminar tutor)

Scientific and Research Activities

• Automata over infinite words: translation from LTL, reduction, transformation, and applications.
• Automatic analysis and verification of software and hardware systems.
• SMT-solving.

Academical Stays

• 2019: A one-week research stay at University of Mons, Belgium.
• 2014, 2015, 2018, 2019: One-week research stays at LRDE, EPITA, France.
• 2008: A one-week research stay at INRIA Rennes, France.
• 2005: A one-week research stay at LIAFA, University Paris 7, France.
• 2005: A three-months research stay at the Institute for Formal Methods in Computer Science, University of Stuttgart, Germany.

Appreciation of Science Community

• 2022: MUNI Scientist Award
• 2017: Rector's award for excellency in teaching, Masaryk University, Brno, Czech Republic.
• 2014: Dean's award for excellency in teaching, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2007: Dean's award for distinguished PhD thesis, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2001: Annual dean's prize, Faculty of Informatics, Masaryk University, Brno, Czech Republic.
• 2001: 2nd place in SVOČ (a Czech mathematical research contest for undergraduate students), category Theoretical Informatics.
• 2000: Annual rector's prize, Masaryk University, Brno, Czech Republic.
• 1999: Annual prize of Section of Mathematics, Faculty of Science, Masaryk University, Brno, Czech Republic.

Selected Publications

• JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Cham: Springer, 2024, s. 234-255. ISBN 978-3-031-57227-2. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57228-9_12. URL info
• AYAZIOVÁ, Paulína a Jan STREJČEK. Witch 3: Validation of Violation Witnesses in the Witness Format 2.0. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 341-346. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_18. URL info
• JONÁŠ, Martin, Jan STREJČEK, Marek TRTÍK a Lukáš URBAN. Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 90-109. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_5. URL info
• JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ a Jan STREJČEK. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 406-411. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_29. URL info
• JONÁŠ, Martin, Jan STREJČEK, Marek TRTÍK a Lukáš URBAN. Fizzer: New Gray-Box Fuzzer. Online. In Dirk Beyer and Ana Cavalcanti. Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings. Cham (Švýcarsko): Springer, 2024, s. 309-313. ISBN 978-3-031-57258-6. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57259-3_17. URL info
• AYAZIOVÁ, Paulína, Dirk BEYER, Marian LINGSCH-ROSENFELD, Martin SPIESSL a Jan STREJČEK. Software Verification Witnesses 2.0. Online. In Thomas Neele and Anton Wijs. Model Checking Software - 30th International Symposium, SPIN 2024. Cham (Švýcarsko): Springer, 2024, s. 184-203. ISBN 978-3-031-66148-8. Dostupné z: https://dx.doi.org/10.1007/978-3-031-66149-5_11. URL info
• SCHWARZOVÁ, Tereza, Jan STREJČEK a Juraj MAJOR. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. Online. In Meena Mahajan and Friedrich Slivovsky. 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, s. 1-20. ISBN 978-3-95977-286-0. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.SAT.2023.23. URL info
• AYAZIOVÁ, Paulína a Jan STREJČEK. Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation. Online. In Sriram Sankaranarayanan and Natasha Sharygina. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2023, s. 523-528. ISBN 978-3-031-30819-2. Dostupné z: https://dx.doi.org/10.1007/978-3-031-30820-8_30. URL info
• AYAZIOVÁ, Paulína, Marek CHALUPA a Jan STREJČEK. Symbiotic-Witch: A Klee-Based Violation Witness Checker. Online. In Dana Fisman and Grigore Rosu. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2022, s. 468-473. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_33. URL info
• CHALUPA, Marek, Vincent MIHALKOVIČ, Anna ŘECHTÁČKOVÁ, Lukáš ZAORAL a Jan STREJČEK. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding. Online. In Dana Fisman and Grigore Rosu. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2022, s. 462-467. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_32. URL info
• BEYER, Dirk a Jan STREJČEK. Case Study on Verification-Witness Validators: Where We Are and Where We Go. Online. In Gagandeep Singh, Caterina Urban. Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022, Proceedings. Cham (Switzerland): Springer, 2022, s. 160-174. ISBN 978-3-031-22307-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-22308-2_8. URL info
• CHALUPA, Marek, Martina VITOVSKÁ, Tomáš JAŠEK, Michael ŠIMÁČEK a Jan STREJČEK. Symbiotic 6: generating test cases by slicing and symbolic execution. International Journal on Software Tools for Technology Transfer. 2021, roč. 23, č. 6, s. 875-877. ISSN 1433-2779. Dostupné z: https://dx.doi.org/10.1007/s10009-020-00573-0. URL info
• CHALUPA, Marek, Jakub NOVÁK a Jan STREJČEK. Symbiotic 8: Parallel and Targeted Test Generation. In Esther Guerra and Mariëlle Stoelinga. Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 368-372. ISBN 978-3-030-71499-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-71500-7_20. URL info
• CHALUPA, Marek, David KLAŠKA, Jan STREJČEK a Lukáš TOMOVIČ. Fast Computation of Strong Control Dependencies. In Alexandra Silva, K. Rustan M. Leino. Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2021, s. 887-910. ISBN 978-3-030-81687-2. Dostupné z: https://dx.doi.org/10.1007/978-3-030-81688-9_41. URL info
• CHALUPA, Marek, Tomáš JAŠEK, Jakub NOVÁK, Anna ŘECHTÁČKOVÁ, Veronika ŠOKOVÁ a Jan STREJČEK. Symbiotic 8: Beyond Symbolic Execution. In Jan Friso Groote, Kim Guldstrand Larsen. Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2021, s. 453-457. ISBN 978-3-030-72012-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-72013-1_31. URL info
• SÍČ, Juraj a Jan STREJČEK. DQBDD: An Efficient BDD-Based DQBF Solver. Online. In Chu-Min Li and Felip Manyà. Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 535-544. ISBN 978-3-030-80222-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-80223-3_36. URL info
• CHALUPA, Marek a Jan STREJČEK. Backward Symbolic Execution with Loop Folding. Online. In Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi. Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 49-76. ISBN 978-3-030-88805-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-88806-0_3. URL info
• CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ. Joint Forces for Memory Safety Checking Revisited. International Journal on Software Tools for Technology Transfer (STTT). Springer, 2020, roč. 22, č. 2, s. 115-133. ISSN 1433-2779. Dostupné z: https://dx.doi.org/10.1007/s10009-019-00526-2. URL info
• CHALUPA, Marek, Tomáš JAŠEK, Lukáš TOMOVIČ, Martin HRUŠKA, Veronika ŠOKOVÁ, Paulína AYAZIOVÁ, Jan STREJČEK a Tomáš VOJNAR. Symbiotic 7: Integration of Predator and More (Competition Contribution). In Armin Biere, David Parker. Tools and Algorithms for the Construction and Analysis of Systems. Německo: Springer, 2020, s. 413-417. ISBN 978-3-030-45236-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-45237-7_31. URL info
• BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to self-loop alternating automata with generic acceptance and back. Theoretical Computer Science. AMSTERDAM: North Holland, 2020, roč. 840, Nov 2020, s. 122-142. ISSN 0304-3975. Dostupné z: https://dx.doi.org/10.1016/j.tcs.2020.07.015. URL info
• JONÁŠ, Martin a Jan STREJČEK. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Online. In Luca Pulina and Martina Seidl. Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. Cham (Switzerland): Springer, 2020, s. 378-393. ISBN 978-3-030-51824-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-51825-7_27. URL info
• BLAHOUDEK, František, Alexandre DURET-LUTZ a Jan STREJČEK. Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. Online. In Shuvendu K. Lahiri and Chao Wang. Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Cham (Switzerland): Springer, 2020, s. 15-27. ISBN 978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8_2. URL info
• JONÁŠ, Martin a Jan STREJČEK. Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. Online. In Isil Dillig, Serdar Tasiran. CAV 2019: Computer Aided Verification. Cham (Switzerland): Springer, 2019, s. 64-73. ISBN 978-3-030-25542-8. Dostupné z: https://dx.doi.org/10.1007/978-3-030-25543-5_4. URL info
• MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ a Tatiana ZBONČÁKOVÁ. ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 357-365. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_21. URL info
• CHALUPA, Marek a Jan STREJČEK. Evaluation of Program Slicing in Software Verification. In Wolfgang Ahrendt, Silvia Lizeth Tapia Tarifa. Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 101-119. ISBN 978-3-030-34967-7. Dostupné z: https://dx.doi.org/10.1007/978-3-030-34968-4_6. URL info
• BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER a Jan STREJČEK. Generic Emptiness Check for Fun and Profit. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 445-461. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_26. URL info
• BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. Online. In Robert Mark Hierons, Mohamed Mosbah. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 152-171. ISBN 978-3-030-32504-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32505-3_10. URL info
• CHALUPA, Marek, Martina VITOVSKÁ a Jan STREJČEK. Symbiotic 5: Boosted Instrumentation (Competition Contribution). In Dirk Beyer and Marieke Huisman. Tools and Algorithms for the Construction and Analysis of Systems, 24th International Conference, Proceedings, Part II. Berlin: Springer, 2018, s. 442-446. ISBN 978-3-319-89963-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-89963-3_29. info
• JONÁŠ, Martin a Jan STREJČEK. On the complexity of the quantified bit-vector arithmetic with binary encoding. Information Processing Letters. Elsevier, 2018, roč. 135, červenec 2018, s. 57-61. ISSN 0020-0190. Dostupné z: https://dx.doi.org/10.1016/j.ipl.2018.02.018. URL info
• CHALUPA, Marek, Jan STREJČEK a Martina VITOVSKÁ. Joint Forces for Memory Safety Checking. In María-del-Mar Gallardo and Pedro Merino. Model Checking Software. SPIN 2018. Cham, Švýcarsko: Springer, 2018, s. 115-132. ISBN 978-3-319-94110-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-94111-0_7. info
• JONÁŠ, Martin a Jan STREJČEK. Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. In Bernd Fischer, Tarmo Uustalu. Theoretical Aspects of Computing – ICTAC 2018. Cham (Switzerland): Springer, 2018, s. 273-291. ISBN 978-3-030-02507-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-02508-3_15. URL info
• JONÁŠ, Martin a Jan STREJČEK. Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?. Online. In Gilles Barthe, Geoff Sutcliffe, Margus Veanes. LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Neuveden: EasyChair, 2018, s. 488-497. ISSN 2398-7340. Dostupné z: https://dx.doi.org/10.29007/spnx. URL info
• BLAHOUDEK, František, Alexandre DURET-LUTZ, Mikuláš KLOKOČKA, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Seminator: A Tool for Semi-Determinization of Omega-Automata. Online. In Thomas Eiter and David Sands. Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017). Neuveden: EasyChair, 2017, s. 356-367. ISSN 2398-7340. Dostupné z: https://dx.doi.org/10.29007/k5nl. URL info
• CHALUPA, Marek, Martina VITOVSKÁ, Martin JONÁŠ, Jiří SLABÝ a Jan STREJČEK. Symbiotic 4: Beyond Reachability (Competition Contribution). In Axel Legay, Tiziana Margaria. Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference. Berlin: Springer Berlin Heidelberg, 2017, s. 385-389. ISBN 978-3-662-54580-5. Dostupné z: https://dx.doi.org/10.1007/978-3-662-54580-5_28. URL info
• CHALUPA, Marek, Martin JONÁŠ, Jiří SLABÝ, Jan STREJČEK a Martina VITOVSKÁ. Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution). In Marsha Chechik and Jean-Francois Raskin. Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Berlin, Heidelberg: Springer, 2016, s. 946-949. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_67. info
• JONÁŠ, Martin a Jan STREJČEK. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Nadia Creignou and Daniel Le Berre. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference. Berlin, Heidelberg: Springer, 2016, s. 267-283. ISBN 978-3-319-40969-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-40970-2_17. info
• ČADEK, Pavel, Jan STREJČEK a Marek TRTÍK. Tighter Loop Bound Analysis. In Cyrille Artho and Axel Legay and Doron Peled. Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Berlin, Heidelberg: Springer, 2016, s. 512-527. ISBN 978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3_32. info
• BABIAK, Tomáš, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, Jan KŘETÍNSKÝ, David MÜLLER, David PARKER a Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, s. 479-486. ISBN 978-3-319-21689-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-21690-4_31. info
• BLAHOUDEK, František, Alexandre DURET-LUTZ, Vojtěch RUJBR a Jan STREJČEK. On Refinement of Büchi Automata for Explicit Model Checking. In Fischer, Bernd and Geldenhuys, Jaco. 2015 International SPIN Symposium on Model Checking of Software. Heidelberg, New York, Dordrecht, London: Springer International Publishing, 2015, s. 66-83. ISBN 978-3-319-23403-8. Dostupné z: https://dx.doi.org/10.1007/978-3-319-23404-5_6. info
• SLABÝ, Jiří a Jan STREJČEK. Symbiotic 2: More Precise Slicing (Competition Contribution). In E. Ábrahám and K. Havelund. Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014. Berlin, Heidelberg: Springer, 2014, s. 415-417. ISBN 978-3-642-54861-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-54862-8_34. info
• BLAHOUDEK, František, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Is there a best Büchi automaton for explicit model checking? In Neha Rungta and Oksana Tkachuk. 2014 International SPIN Symposium on Model Checking of Software. New York: ACM, 2014, s. 68-76. ISBN 978-1-4503-2452-6. Dostupné z: https://dx.doi.org/10.1145/2632362.2632377. info
• TRTÍK, Marek a Jan STREJČEK. Symbolic Memory with Pointers. In Franck Cassez and Jean-Francois Raskin. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Berlin Heidelberg: Springer, 2014, s. 380-395. ISBN 978-3-319-11935-9. Dostupné z: https://dx.doi.org/10.1007/978-3-319-11936-6_27. info
• SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. ClabureDB: Classified Bug-Reports Database Tool for Developers of Program Analysis Tools. In Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni. Verification, Model Checking, and Abstract Interpretation: 14th International Conference, VMCAI 2013. Berlin, Heidelberg: Springer, 2013, s. 268-274. ISBN 978-3-642-35872-2. Dostupné z: https://dx.doi.org/10.1007/978-3-642-35873-9_17. info
• SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). In Nir Piterman, Scott A. Smolka. Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. Berlin, Heidelberg: Springer, 2013, s. 630-632. ISBN 978-3-642-36741-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-36742-7_50. info
• BABIAK, Tomáš, Thomas BADIE, Alexandre DURET-LUTZ, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Compositional Approach to Suspension and Other Improvements to LTL Translation. In Ezio Bartocci, C. R. Ramakrishnan. Model Checking Software - 20th International Symposium, SPIN 2013. LNCS 7976. Berlin Heidelberg: Springer, 2013, s. 81-98. ISBN 978-3-642-39175-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39176-7_6. info
• SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Compact Symbolic Execution. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer, 2013, s. 193-207. ISBN 978-3-319-02443-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-02444-8_15. info
• BLAHOUDEK, František, Tomáš BABIAK, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer, 2013, s. 24-38. ISBN 978-3-319-02443-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-02444-8_4. info
• BLAHOUDEK, František, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Comparison of LTL to Deterministic Rabin Automata Translators. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov. Logic for Programming Artificial Intelligence and Reasoning, LPAR-19. Berlin Heidelberg: Springer, 2013, s. 164-172. ISBN 978-3-642-45220-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-45221-5_12. info
• BABIAK, Tomáš, Jan STREJČEK a Vojtěch ŘEHÁK. Almost linear Büchi automata. Mathematical Structures in Computer Science. Cambridge: Cambridge University Press, 2012, roč. 22, č. 2, s. 203-235. ISSN 0960-1295. Dostupné z: https://dx.doi.org/10.1017/S0960129511000399. URL info
• BABIAK, Tomáš, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan, Barbara König. TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2012, s. 95-109. ISBN 978-3-642-28755-8. Dostupné z: https://dx.doi.org/10.1007/978-3-642-28756-5_8. URL info
• SLABÝ, Jiří, Jan STREJČEK a Marek TRTÍK. Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. In Mariëlle Stoelinga, Ralf Pinger. Formal Methods for Industrial Critical systems: 17th International Workshop, FMICS 2012. Berlin, Heidelberg: Springer, 2012, s. 207-221. ISBN 978-3-642-32468-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-32469-7_14. URL info
• STREJČEK, Jan a Marek TRTÍK. Abstracting Path Conditions. In Mats Per Erik Heimdahl, Zhendong Su. Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012. New York, NY, USA: ACM, 2012, s. 155-165. ISBN 978-1-4503-1454-1. Dostupné z: https://dx.doi.org/10.1145/2338965.2336772. URL info
• ŘEHÁK, Vojtěch, Petr SLOVÁK, Jan STREJČEK a Loïc HÉLOUËT. Decidable Race Condition and Open Coregions in HMSC. In Jochen Küster, Emilio Tuosto. Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2010). Paphos, Kypr: ECEASST, 2010, 12 s. ISSN 1863-2122. URL info
• BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. Acta informatica. Berlin: Springer-Verlag, 2009, roč. 46, č. 1, s. 1-28. ISSN 0001-5903. URL info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). 2009. vyd. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009, s. 105-117. ISSN 1571-0661. URL info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Reachability is decidable for weakly extended process rewrite systems. Information and Computation. Elsevier, 2009, roč. 207, č. 6, s. 671-680. ISSN 0890-5401. URL info
• BABIAK, Tomáš, Vojtěch ŘEHÁK a Jan STREJČEK. Almost Linear Büchi Automata. In Proceedings 16th International Workshop on Expressiveness in Concurrency 2009 (EXPRESS'09). 1st ed. internet: EPTCS, 2009, s. 16-25. ISSN 2075-2180. DOI info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science. Amsterdam, North Holland: Elsevier Science Publishers, 2008, roč. 394, 1-2, s. 134-140. ISSN 0304-3975. info
• BOUAJJANI, Ahmed, Jan STREJČEK a Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS 2006). Neuveden: Elsevier, 2007, s. 47-64. ISSN 1571-0661. URL info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Proc. of 9th Internat. Workshop on Verification of Infinite-State Systems. 2007. info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. In Proceedings of the 7th International Workshop on Verification of Infinite-State Systems (INFINITY'05). 2006. vyd. Amsterdam, The Netherlands: Elsevier Science, 2006, s. 17-36. ISSN 1571-0661. URL info
• BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin: Springer-Verlag, 2006, s. 248-259. ISBN 978-3-540-49994-7. info
• BOUAJJANI, Ahmed, Jan STREJČEK a Tayssir TOUILI. On Symbolic Verification of Weakly Extended PAD. In Preliminary Proceedings - 13th International Workshow on Expressiveness in Concurrency - EXPRESS'06. London: Imperial College London, 2006, s. 29-41. info
• KUČERA, Antonín a Jan STREJČEK. Characteristic Patterns for LTL. P. Vojtas, M. Bielikova, B. Charron-Bost, O. Sykora (Eds.). In SOFSEM 2005: Theory and Practice of Computer Science. Berlin, Heidelberg: Springer-Verlag, 2005, s. 239-249. ISBN 3-540-24302-X. info
• KUČERA, Antonín a Jan STREJČEK. The stuttering principle revisited. Acta informatica. Berlin: Springer-Verlag, 2005, roč. 41, 7/8, s. 415-434. ISSN 0001-5903. info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Reachability of Hennessy - Milner properties for weakly extended PRS. In FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005, s. 213-224. ISBN 3-540-30495-9. info
• BOUAJJANI, Ahmed, Javier ESPARZA, Stefan SCHWOON a Jan STREJČEK. Reachability Analysis of Multithreaded Software with Asynchronous Communication. In FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005, s. 348-359. ISBN 3-540-30495-9. info
• PELÁNEK, Radek a Jan STREJČEK. Deeper Connections between LTL and Alternating Automata. In Implementation and Application of Automata. Berlin, Heidelberg: Springer-Verlag, 2005, s. 238-249. ISBN 978-3-540-31023-5. info
• STREJČEK, Jan. Linear Temporal Logic: Expressiveness and Model Checking. Faculty of Informatics, Masaryk University, 2005, 148 s. info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. Extended Process Rewrite Systems: Expressiveness and Reachability. In CONCUR 2004 - Concurrency Theory. LNCS 3170. Berlin, Heidelberg, New York: Springer, 2004, s. 355-370. ISBN 3-540-22940-X. info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In INFINITY'2003: 5th International Workshop on Verification of Infinite-State Systems. 2004. vyd. Amsterdam, The Netherlands: Elsevier Science, 2004, s. 75-88. ISSN 1571-0661. URL info
• KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. In Prelim.Proc.of the 5th Internat.Workshop on Verification of Infinite-State Systems (INFINITY'2003). Marseille, France: Universite de Provence, Marseille, 2003, s. 73-86. info
• KUČERA, Antonín a Jan STREJČEK. The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. J. Bradfield (Ed.). In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'02). Berlin: Springer, 2002, s. 276-291. ISBN 3-540-44240-5. info
• CRHOVÁ, Jitka, Pavel KRČÁL, Jan STREJČEK, David ŠAFRÁNEK a Pavel ŠIMEČEK. YAHODA: verification tools database. In Proceedings of Tools Day. Brno: FI MU, 2002, s. 99-103. FI MU Report Series info
• STREJČEK, Jan. Boundaries and Efficiency of Verification. In Proceedings of summer school MOVEP 2002. Nantes (France): IRCCyN, Ecole Centrale de Nantes, France, 2002, s. 403-408. info
• STREJČEK, Jan. Models of infinite-state systems with constraints. Brno, 2001, iii, 44. info
• STREJČEK, Jan. Rewrite Systems with Constraints. In EXPRESS'01 the 8th International Workshop on Expressiveness in Concurrency. Aalborg (Denmark): Elsevier Science, 2001, s. 1-20. URL info

2023/11/10