Jan Strejček - Publications

[ Journal papers | Proceedings papers | Technical reports & unreviewed papers | Thesis ]
Journal papers
  1. M. Jonáš and J. Strejček: Truncating abstraction of bit-vector operations for BDD-based SMT solvers, Theoretical Computer Science 1008 (2024) 114664, 2024. [DOI link, PDF]

  2. M. Chalupa, M. Vitovská, T. Jašek, M. Šimáček, and J. Strejček: Symbiotic 6: Generating Test-Cases by Slicing and Symbolic Execution, International Journal on Software Tools for Technology Transfer 23(6): 875-877, 2021. [DOI link, preprint PDF]

  3. F. Blahoudek, J. Major, and J. Strejček: LTL to Self-Loop Alternating Automata with Generic Acceptance and Back. Theoretical Computer Science 840:122-142, 2020. [DOI link, preprint PDF]

  4. M. Chalupa, J. Strejček, and M. Vitovská: Joint Forces For Memory Safety Checking Revisited, International Journal on Software Tools for Technology Transfer 22(2): 115-133, 2020. [DOI link, preprint PDF]

  5. M. Jonáš and J. Strejček: On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoding, Information Processing Letters 135:57-61, 2018. [DOI link, PDF]

  6. T. Babiak, V. Řehák, and J. Strejček: Almost Linear Büchi Automata, Mathematical Structures in Computer Science 22(02):203-235, 2012. [DOI link, preprint PDF]

  7. M. Křetínský, V. Řehák, and J. Strejček: Reachability is Decidable for Weakly Extended Process Rewrite Systems. Information and Computation 207(6):671-680, 2009. [DOI link, preprint PDF]

  8. L. Bozzelli, M. Křetínský, V. Řehák, and J. Strejček: On decidability of LTL model checking for process rewrite systems. Acta Informatica 46(1):1-28, 2009. [DOI link, preprint PDF]

  9. M. Křetínský, V. Řehák, and J. Strejček: Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science 394(1-2):134-140, 2008. [DOI link, preprint PDF]

  10. A. Kučera and J. Strejček: The Stuttering Principle Revisited. Acta Informatica 41(7-8):415-434, 2005. [PDF]
Proceedings papers
  1. M. Jonáš, J. Strejček, A. Griggio: Combining Symbolic Execution with Predicate Abstraction and CEGAR, in Proceedings of FMCAD 2024, pages 272-280, TU Wien Academic Press, 2024. [DOI link, PDF]

  2. P. Ayaziová, D. Beyer, M. Lingsch-Rosenfeld, M. Spiessl, and J. Strejček: Software Verification Witnesses 2.0, in Proceedings of SPIN 2024, volume 14624 of LNCS, pages 184-203. Springer, 2024. [DOI link, PDF]

  3. M. Jonáš, J. Strejček, M. Trtík, and L. Urban: Fizzer: New Gray-Box Fuzzer (Competition Contribution), in Proceedings of FASE 2024, volume 14573 of LNCS, pages 309-313. Springer, 2024. [DOI link, PDF]

  4. M. Jonáš, K. Kumor, J. Novák, J. Sedláček, M. Trtík, L. Zaoral, P. Ayaziová, and J. Strejček: Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution (Competition Contribution), in Proceedings of TACAS 2024, volume 14572 of LNCS, pages 406-411. Springer, 2024. [DOI link, PDF]

  5. P. Ayaziová and J. Strejček: Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 (Competition Contribution), in Proceedings of TACAS 2024, volume 14572 of LNCS, pages 341-346. Springer, 2024. [DOI link, PDF]

  6. M. Jonáš, J. Strejček, M. Trtík, and L. Urban: Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage, in Proceedings of TACAS 2024, volume 14572 of LNCS, pages 90-109. Springer, 2024. [DOI link, PDF]

  7. M. Jankola and J. Strejček: Tighter Construction of Tight Büchi Automata, in Proceedings of FoSSaCS 2024, volume 14574 of LNCS, pages 234-255. Springer, 2024. [DOI link, PDF]

  8. T. Schwarzová, J. Strejček, and J. Major: Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving, in Proceedings of SAT 2023, volume 271 of LIPIcs. Schloss Dagstuhl, 2023. [DOI link, PDF]

  9. P. Ayaziová and J. Strejček: Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution), in Proceedings of TACAS 2023, volume 13994 of LNCS, pages 523-528. Springer, 2023. [DOI link, PDF]

  10. D. Beyer and J. Strejček: Case Study on Verification-Witness Validators: Where We Are and Where We Go, in Proceedings of SAS 2022, volume 13790 of LNCS, pages 160-174. Springer, 2022. [DOI link, PDF]

  11. M. Chalupa, V. Mihalkovič, A. Řechtáčková, L. Zaoral, and J. Strejček: Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding (Competition Contribution), in Proceedings of TACAS 2022, volume 13244 of LNCS, pages 462-467. Springer, 2022. [DOI link, PDF]

  12. P. Ayaziová, M. Chalupa, and J. Strejček: Symbiotic-Witch: A Klee-Based Violation Witness Checker (Competition Contribution), in Proceedings of TACAS 2022, volume 13244 of LNCS, pages 468-473. Springer, 2022. [DOI link, PDF]

  13. M. Chalupa and J. Strejček: Backward Symbolic Execution with Loop Folding, in Proceedings of SAS 2021, volume 12913 of LNCS, pages 49-76. Springer, 2021. [DOI link, preprint PDF]

  14. J. Síč and J. Strejček: DQBDD: An Efficient BDD-Based DQBF Solver, in Proceedings of SAT 2021, volume 12831 of LNCS, pages 535-544. Springer, 2021. [DOI link, preprint PDF]

  15. M. Chalupa, D. Klaška, J. Strejček, and L. Tomovič: Fast Computation of Strong Control Dependencies, in Proceedings of CAV 2021, volume 12760 of LNCS, pages 887-910. Springer, 2021. [DOI link, PDF]

  16. M. Chalupa, J. Novák, and J. Strejček: Symbiotic 8: Parallel and Targeted Test Generation (Competition Contribution), in Proceedings of FASE 2021, volume 12649 of LNCS, pages 368-372. Springer, 2021. [DOI link, PDF]

  17. M. Chalupa, T. Jašek, J. Novák, A. Řechtáčková, V. Šoková, and J. Strejček: Symbiotic 8: Beyond Symbolic Execution (Competition Contribution), in Proceedings of TACAS 2021, volume 12652 of LNCS, pages 453-457. Springer, 2021. [DOI link, PDF]

  18. M. Jonáš and J. Strejček: Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions, in Proceedings of SAT 2020, volume 12178 of LNCS, pages 378-393. Springer, 2020. [DOI link, preprint PDF, corresponding data]

  19. F. Blahoudek, A. Duret-Lutz, and J. Strejček: Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-Determinization, in Proceedings of CAV 2020, volume 12225 of LNCS, pages 15-27. Springer, 2020. [DOI link, preprint PDF]

  20. M. Chalupa, T. Jašek, L. Tomovič, M. Hruška, V. Šoková, P. Ayaziová, J. Strejček, and T. Vojnar: Symbiotic 7: Integration of Predator and More (Competition Contribution), in Proceedings of TACAS 2020, volume 12079 of LNCS, pages 413-417. Springer, 2020. [DOI link, PDF]

  21. M. Chalupa and J. Strejček: Evaluation of Program Slicing in Software Verification, in Proceedings of iFM 2019, volume 11918 of LNCS, pages 101-119. Springer, 2019. [DOI link, preprint PDF]

  22. F. Blahoudek, J. Major, and J. Strejček: LTL to Smaller Self-Loop Alternating Automata and Back, in Proceedings of ICTAC 2019, volume 11884 of LNCS, pages 152-171. Springer, 2019. Received the best paper award of ICTAC 2019. [DOI link, full version on arXiv]

  23. Ch. Baier, F. Blahoudek, A. Duret-Lutz, J. Klein, D. Mueller, and J. Strejček: Generic Emptiness Check for Fun and Profit, in Proceedings of ATVA 2019, volume 11781 of LNCS, pages 445-461. Springer, 2019. [DOI link, corrected and extended version PDF]

  24. J. Major, F. Blahoudek, J. Strejček, M. Sasaráková, and T. Zbončáková: ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata, in Proceedings of ATVA 2019, volume 11781 of LNCS, pages 357-365. Springer, 2019. [DOI link, preprint PDF]

  25. M. Jonáš and J. Strejček: Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors, in Proceedings of CAV 2019, volume 11562 of LNCS, pages 64-73. Springer, 2019. [DOI link, preprint PDF]

  26. M. Jonáš and J. Strejček: Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes?, in Proceedings of LPAR 2018, EPiC Series in Computing 57, pages 488-497, 2018. [link, PDF]

  27. M. Jonáš and J. Strejček: Abstraction of Bit-Vector Operations for BDD-based SMT Solvers, in Proceedings of ICTAC 2018, volume 11187 of LNCS, pages 273-291. Springer, 2018. [DOI link, corrected version PDF, corresponding data]

  28. M. Chalupa, J. Strejček, and M. Vitovská: Joint Forces For Memory Safety Checking, in Proceedings of SPIN 2018, volume 10869 of LNCS, pages 115-132. Springer, 2018. [DOI link, preprint PDF]

  29. M. Chalupa, M. Vitovská, and J. Strejček: Symbiotic 5: Boosted Instrumentation (Competition Contribution), in Proceedings of TACAS 2018, volume 10806 of LNCS, pages 442-226. Springer, 2018. [DOI link, preprint PDF]

  30. M. Jonáš and J. Strejček: On Simplification of Formulas with Unconstrained Variables and Quantifiers, in Proceedings of SAT 2017, volume 10491 of LNCS, pages 364-379. Springer, 2017. [DOI link, preprint PDF, corresponding data]

  31. F. Blahoudek, A. Duret-Lutz, M. Klokočka, M. Křetínský, and J. Strejček: Seminator: A Tool for Semi-Determinization of Omega-Automata, in Proceedings of LPAR 2017, EPiC Series in Computing 46, pages 356-367, 2017. [link, PDF]

  32. M. Chalupa, M. Vitovská, M. Jonáš, J. Slaby, and J. Strejček: Symbiotic 4: Beyond Reachability (Competition Contribution), in Proceedings of TACAS 2017, volume 10206 of LNCS, pages 385-389. Springer, 2017. [DOI link, preprint PDF]

  33. P. Čadek, J. Strejček, and M. Trtík: Tighter Loop Bound Analysis, in Proceedings of ATVA 2016, volume 9938 of LNCS, pages 512-527. Springer, 2016. [DOI link, preprint PDF]

  34. M. Jonáš and J. Strejček: Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams, in Proceedings of SAT 2016, volume 9710 of LNCS, pages 267-283. Springer, 2016. [DOI link, preprint PDF, corresponding data]

  35. M. Chalupa, M. Jonáš, J. Slaby, J. Strejček, and M. Vitovská: Symbiotic 3: New Slicer and Error-Witness Generation (Competition Contribution), in Proceedings of TACAS 2016, volume 9636 of LNCS, pages 946-949. Springer, 2016. [DOI link, preprint PDF]

  36. F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and M.-H. Tsai: Complementing Semi-Deterministic Büchi Automata, in Proceedings of TACAS 2016, volume 9636 of LNCS, pages 770-787. Springer, 2016. [DOI link, preprint PDF]

  37. F. Blahoudek, A. Duret-Lutz, V. Rujbr, and J. Strejček: On Refinement of Büchi Automata for Explicit Model Checking, in Proceedings of SPIN 2015, volume 9232 of LNCS, pages 66-83. Springer, 2015. [DOI link, corrected version PDF, corresponding data]

  38. T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. Křetínský, D. Mueller, D. Parker, and J. Strejček: The Hanoi Omega-Automata Format, in Proceedings of CAV 2015, volume 9206 of LNCS, pages 479-486. Springer, 2015. [DOI link, preprint PDF, format specification]

  39. M. Trtík and J. Strejček: Symbolic Memory with Pointers, in Proceedings of ATVA 2014, volume 8837 of LNCS, pages 380-395. Springer, 2014. [DOI link, preprint PDF]

  40. F. Blahoudek, A. Duret-Lutz, M. Křetínský, and J. Strejček: Is There a Best Büchi Automaton for Explicit Model Checking?, in Proceedings of SPIN 2014, pages 68-76. ACM, 2014. [DOI link, preprint PDF, corresponding data]

  41. J. Slaby and J. Strejček: Symbiotic 2: More Precise Slicing (Competition Contribution), in Proceedings of TACAS 2014, volume 8413 of LNCS, pages 415-417. Springer, 2014. [DOI link, preprint PDF]

  42. F. Blahoudek, M. Křetínský, and J. Strejček: Comparison of LTL to Deterministic Rabin Automata Translators, in Proceedings of LPAR 2013, volume 8312 of LNCS, pages 164-172. Springer, 2013. [DOI link, preprint PDF]

  43. T. Babiak, F. Blahoudek, M. Křetínský, and J. Strejček: Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment, in Proceedings of ATVA 2013, volume 8172 of LNCS, pages 24-39. Springer, 2013. [DOI link, preprint PDF, full version on arXiv]

  44. J. Slaby, J. Strejček, and M. Trtík: Compact Symbolic Execution, in Proceedings of ATVA 2013, volume 8172 of LNCS, pages 193-207. Springer, 2013. [DOI link, preprint PDF, full version on arXiv]

  45. T. Babiak, T. Badie, A. Duret-Lutz, M. Křetínský, and J. Strejček: Compositional Approach to Suspension and Other Improvements to LTL Translation, in Proceedings of SPIN 2013, volume 7976 of LNCS, pages 81-98. Springer, 2013. [DOI link, corrected version PDF]

  46. J. Slaby, J. Strejček, and M. Trtík: Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution (Competition Contribution), in Proceedings of TACAS 2013, volume 7795 of LNCS, pages 630-632. Springer, 2013. [DOI link, preprint PDF]

  47. J. Slaby, J. Strejček, and M. Trtík: ClabureDB: Classified Bug-Reports Database (Tool for Developers of Program Analysis Tools), in Proceedings of VMCAI 2013, volume 7737 of LNCS, pages 268-274. Springer, 2013. [DOI link, preprint PDF]

  48. J. Slaby, J. Strejček, and M. Trtík: Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution, in Proceedings of FMICS 2012, volume 7437 of LNCS, pages 207-221. Springer, 2012. [DOI link, preprint PDF]

  49. J. Strejček and M. Trtík: Abstracting Path Conditions, in Proceedings of ISSTA 2012, pages 155-165, ACM, 2012. [DOI link, preprint PDF]

  50. T. Babiak, M. Křetínský, V. Řehák, and J. Strejček: LTL to Büchi Automata Translation: Fast and More Deterministic, in Proceedings of TACAS 2012, volume 7214 of LNCS, pages 95-109. Springer, 2012. [DOI link, preprint PDF, full version on arXiv]

  51. V. Řehák, P. Slovák, J. Strejček, and L. Hélouët: Decidable Race Condition and Open Coregions in HMSC, in Proceedings of GT-VMT 2010, volume 29 of Electronic Communications of the EASST, 12 pages, 2010. [PDF]

  52. T. Babiak, V. Řehák, and J. Strejček: Almost Linear Büchi Automata, in Proceedings of EXPRESS 2009, volume 8 of EPTCS, pages 16-25, 2009. [DOI link, PDF]

  53. M. Křetínský, V. Řehák, and J. Strejček: On Decidability of LTL+Past Model Checking for Process Rewrite Systems, in Proceedings of INFINITY 2007, volume 239 of ENTCS, pages 105-117. Elsevier, 2009. [DOI link, preprint PDF]

  54. L. Bozzelli, M. Křetínský, V. Řehák, and J. Strejček: On Decidability of LTL Model Checking for Process Rewrite Systems, in Proceedings of FSTTCS 2006, volume 4337 of LNCS, pages 248-259. Springer, 2006. [PDF]

  55. A. Bouajjani, J. Strejček, and T. Touili: On Symbolic Verification of Weakly Extended PAD, in Proceedings of EXPRESS 2006, volume 175(3) of ENTCS, pages 47-64. Elsevier Science Publishers, 2007. [DOI link, preprint PDF; full version can be found below as LIAFA tech. report 2006-001]

  56. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejček: Reachability analysis of multithreaded software with asynchronous communication, in Proceedings of Software Verification: Infinite-State Model Checking and Static Program Analysis, Dagstuhl Seminar Proceedings 06081, 18 pages. IBFI, 2006. [PDF]

  57. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejček: Reachability Analysis of Multithreaded Software with Asynchronous Communication, in Proceedings of FSTTCS 2005, volume 3821 of LNCS, pages 348-359. Springer, 2005. [PDF]

  58. M. Křetínský, V. Řehák, and J. Strejček: Reachability of Hennessy-Milner Properties for Weakly Extended PRS, in Proceedings of FSTTCS 2005, volume 3821 of LNCS, pages 213-224. Springer, 2005. [PDF]

  59. M. Křetínský, V. Řehák, and J. Strejček: Refining the Undecidability Border of Weak Bisimilarity, in Proceedings of INFINITY 2005, volume 149 of ENTCS, pages 17-36. Elsevier Science Publishers, 2006. [Elsevier web, preprint PDF; full version can be found below as tech. report FIMU-RS-2005-06]

  60. R. Pelánek and J. Strejček: Deeper Connections between LTL and Alternating Automata, in Proceedings of CIAA 2005, volume 3845 of LNCS, pages 238-249. Springer, 2006. [PDF]

  61. A. Kučera and J. Strejček: Characteristic Patterns for LTL, in Proceedings of SOFSEM 2005, volume 3381 of LNCS, pages 239-249. Springer, 2005. [postscript]

  62. M. Křetínský, V. Řehák, and J. Strejček: Extended Process Rewrite Systems: Expressiveness and Reachability, in Proceedings of CONCUR 2004, volume 3170 of LNCS, pages 355-370. Springer, 2004. [postscript]

  63. M. Křetínský, V. Řehák, and J. Strejček: On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit, in Proceedings of INFINITY 2003, volume 98 of ENTCS, pages 75-88. Elsevier Science Publishers, 2003. [full version can be found below as tech. report FIMU-RS-2003-05]

  64. A. Kučera and J. Strejček: The Stuttering Principle Revisited: On the Expressiveness of Nested X and U operators in the Logic LTL, in Proceedings of CSL 2002, volume 2471 of LNCS, pages 276-291. Springer, 2002. [postscript]

  65. J. Crhová, P. Krčál, J. Strejček, D. Šafránek, and P. Šimeček: YAHODA: verification tools database, in Proceedings of Tools Day, FI MU Report Series, FIMU-RS-2002-05, pages 99-103. 2002. [postscript]

  66. J. Strejček: Boundaries and Efficiency of Verification, in Proceedings of summer school on Modelling and Verification of Parallel processes (MOVEP'02), pages 403-408. IRCCyN, Ecole Centrale de Nantes, 2002. [postscript]

  67. J. Strejček: Rewrite Systems with Constraints, in Proceedings of EXPRESS 2001, volume 52 of ENTCS, 20 pages. Elsevier Science Publishers, 2002. [preprint postscript]
Technical reports & unreviewed papers
  1. M. Vitovská, M. Chalupa, and J. Strejček: SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode, 2018. [arXiv:1810.12617, PDF]

  2. T. Babiak, M. Křetínský, V. Řehák, and J. Strejček: A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness, 2010. [arXiv:1011.4214, PDF]

  3. V. Řehák, P. Slovak, J. Strejček, and L. Helouet: Decidable Race Condition for HMSC, FI MU Report Series, FIMU-RS-2009-10, 2009. [PDF]

  4. L. Bozzelli, M. Křetínský, V. Řehák, and J. Strejček: On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems, FI MU Report Series, FIMU-RS-2006-05, 2006. Full version of FSTTCS'06 paper. [PDF]

  5. A. Bouajjani, J. Strejček, and T. Touili: On Symbolic Verification of Weakly Extended PAD, Technical Report 2006-001, LIAFA, CNRS and University of Paris 7, 2006. Full version of EXPRESS'06 paper. [PDF]

  6. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejček: Reachability Analysis of Multithreaded Software with Asynchronous Communication, Technical Report 2005/06, Universität Stuttgart, Facultät Informatik, Elektrotechnik und Informationstechnik, November 2005. Full version of FSTTCS'05 paper. [postscript]

  7. M. Křetínský, V. Řehák, and J. Strejček: Refining the Undecidability Border of Weak Bisimilarity, FI MU Report Series, FIMU-RS-2005-06, 2005. Full version of INFINITY'05 paper. [postscript]

  8. A. Kučera and J. Strejček: Characteristic Patterns for LTL, FI MU Report Series, FIMU-RS-2004-10, 2004. Full version of SOFSEM'05 paper. [postscript]

  9. R. Pelánek and J. Strejček: Deeper Connections between LTL and Alternating Automata, FI MU Report Series, FIMU-RS-2004-08, 2004. [postscript]

  10. A. Kučera and J. Strejček: An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator, FI MU Report Series, FIMU-RS-2004-04, 2004. [postscript]

  11. M. Křetínský, V. Řehák, and J. Strejček: On the Expressive Power of Extended Process Rewrite Systems, Technical Report RS-04-07, Basic Research in Computer Science, Aarhus, Denmark, 2004. [postscript]

  12. M. Křetínský, V. Řehák, and J. Strejček: Process Rewrite Systems with Weak Finite-State Unit, FI MU Report Series, FIMU-RS-2003-05, 2003. Full version of INFINITY'03 paper. [postscript]

  13. A. Kučera and J. Strejček: The Stuttering Principle Revisited: On the Expressiveness of Nested X and U operators in the Logic LTL, FI MU Report Series, FIMU-RS-2002-03, 2002. Full version of CSL'02 paper. [postscript]

  14. J. Strejček: Constrained Rewrite Transition Systems, FI MU Report Series, FIMU-RS-2000-12, 2000. Full version of master's thesis. [postscript]
Thesis
  1. Linear Temporal Logic: Expressiveness and Model Checking, Ph.D. thesis, Faculty of Informatics, Masaryk University in Brno, 2004. [postscript, PDF]

  2. Models of Infinite-State Systems with Constraints, Master's thesis, Faculty of Informatics, Masaryk University in Brno, 2001. [postscript]

  3. Constrained Rewrite Transition Systems, Master's thesis, Faculty of Science, Masaryk University in Brno, 2000. [postscript]
strejcek@fi.muni.cz