Jan Strejcek - Publications

[ Journal papers | Proceedings papers | Technical reports & unreviewed papers | Thesis ]

Journal papers
  1. T. Babiak, V. Rehak, and J. Strejcek: Almost Linear Büchi Automata, Mathematical Structures in Computer Science 22(02):203-235, 2012. [DOI link, preprint PDF]

  2. M. Kretinsky, V. Rehak, and J. Strejcek: Reachability is Decidable for Weakly Extended Process Rewrite Systems. Information and Computation 207(6):671-680, 2009. [DOI link, preprint PDF]

  3. L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek: On decidability of LTL model checking for process rewrite systems. Acta Informatica 46(1):1-28, 2009. [DOI link, preprint PDF]

  4. M. Kretinsky, V. Rehak, and J. Strejcek: Petri Nets Are Less Expressive Than State-Extended PA. Theoretical Computer Science 394(1-2):134-140, 2008. [DOI link, preprint PDF]

  5. A. Kucera and J. Strejcek: The Stuttering Principle Revisited. Acta Informatica 41(7-8):415-434, 2005. [PDF]

Proceedings papers
  1. M. Jonas and J. Strejcek: On Simplification of Formulas with Unconstrained Variables and Quantifiers, in Proceedings of SAT 2017, LNCS. Springer, 2017. To appear. [preprint PDF]

  2. F. Blahoudek, A. Duret-Lutz, M. Klokocka, M. Kretinsky, and J. Strejcek: Seminator: A Tool for Semi-Determinization of Omega-Automata, in Proceedings of LPAR 2017, EPiC Series in Computing 46, pages 356-367, 2017. [PDF]

  3. M. Chalupa, M. Vitovska, M. Jonas, J. Slaby, and J. Strejcek: Symbiotic 4: Beyond Reachability (Competition Contribution), in Proceedings of TACAS 2017, volume 10206 of LNCS, pages 385-389. Springer, 2017. [DOI link, preprint PDF]

  4. P. Cadek, J. Strejcek, and M. Trtik: Tighter Loop Bound Analysis, in Proceedings of ATVA 2016, volume 9938 of LNCS, pages 512-527. Springer, 2016. [DOI link, preprint PDF]

  5. M. Jonas and J. Strejcek: 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]

  6. M. Chalupa, M. Jonas, J. Slaby, J. Strejcek, and M. Vitovska: 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]

  7. F. Blahoudek, M. Heizmann, S. Schewe, J. Strejcek, 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]

  8. F. Blahoudek, A. Duret-Lutz, V. Rujbr, and J. Strejcek: 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]

  9. T. Babiak, F. Blahoudek, A. Duret-Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, and J. Strejcek: 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]

  10. M. Trtik and J. Strejcek: Symbolic Memory with Pointers, in Proceedings of ATVA 2014, volume 8837 of LNCS, pages 380-395. Springer, 2014. [DOI link, preprint PDF]

  11. F. Blahoudek, A. Duret-Lutz, M. Kretinsky, and J. Strejcek: 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]

  12. J. Slaby and J. Strejcek: 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]

  13. F. Blahoudek, M. Kretinsky, and J. Strejcek: 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]

  14. T. Babiak, F. Blahoudek, M. Kretinsky, and J. Strejcek: 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]

  15. J. Slaby, J. Strejcek, and M. Trtik: 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]

  16. T. Babiak, Th. Badie, A. Duret-Lutz, M. Kretinsky, and J. Strejcek: 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]

  17. J. Slaby, J. Strejcek, and M. Trtik: 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]

  18. J. Slaby, J. Strejcek, and M. Trtik: 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]

  19. J. Slaby, J. Strejcek, and M. Trtik: 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]

  20. J. Strejcek and M. Trtik: Abstracting Path Conditions, in Proceedings of ISSTA 2012, pages 155-165, ACM, 2012. [DOI link, preprint PDF]

  21. T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek: 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]

  22. V. Rehak, P. Slovak, J. Strejcek, and L. Helouet: 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]

  23. T. Babiak, V. Rehak, and J. Strejcek: Almost Linear Büchi Automata, in Proceedings of EXPRESS 2009, volume 8 of EPTCS, pages 16-25, 2009. [DOI link, PDF]

  24. M. Kretinsky, V. Rehak, and J. Strejcek: 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]

  25. L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek: 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]

  26. A. Bouajjani, J. Strejcek, 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]

  27. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek: 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]

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

  29. M. Kretinsky, V. Rehak, and J. Strejcek: Reachability of Hennessy-Milner Properties for Weakly Extended PRS, in Proceedings of FSTTCS 2005, volume 3821 of LNCS, pages 213-224. Springer, 2005. [PDF]

  30. M. Kretinsky, V. Rehak, and J. Strejcek: 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]

  31. R. Pelanek and J. Strejcek: Deeper Connections between LTL and Alternating Automata, in Proceedings of CIAA 2005, volume 3845 of LNCS, pages 238-249. Springer, 2006. [PDF]

  32. A. Kucera and J. Strejcek: Characteristic Patterns for LTL, in SOFSEM 2005: Theory and Practice of Computer Science, 31st Conference on Current Trends in Theory and Practice of Computer Science, volume 3381 of LNCS, pages 239-249. Springer, 2005. [postscript]

  33. M. Kretinsky, V. Rehak, and J. Strejcek: Extended Process Rewrite Systems: Expressiveness and Reachability, in CONCUR 2004 - Concurrency Theory, volume 3170 of LNCS pages 355-370. Springer, 2004. [postscript]

  34. M. Kretinsky, V. Rehak, and J. Strejcek: 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, volume 98 of ENTCS, pages 75-88. Elsevier Science Publishers, 2003. [full version can be found below as tech. report FIMU-RS-2003-05]

  35. A. Kucera and J. Strejcek: The Stuttering Principle Revisited: On the Expressiveness of Nested X and U operators in the Logic LTL, in CSL 2002: 11th Annual Conference of the European Association for Computer Science Logic, volume 2471 of LNCS, pages 276-291. Springer, 2002. [postscript]

  36. J. Crhova, P. Krcal, J. Strejcek, D. Safranek, and P. Simecek: YAHODA: verification tools database, in Proceedings of Tools Day, FI MU Report Series, FIMU-RS-2002-05, pages 99-103. 2002. [postscript]

  37. J. Strejcek: 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]

  38. J. Strejcek: Rewrite Systems with Constraints, in Proceedings of EXPRESS'01: 8th International Workshop on Expressiveness in Concurrency, volume 52 of ENTCS, 20 pages. Elsevier Science Publishers, 2002. [preprint postscript]

Technical reports & unreviewed papers
  1. T. Babiak, M. Kretinsky, V. Rehak, and J. Strejcek: A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness, 2010. [arXiv:1011.4214, PDF]

  2. V. Rehak, P. Slovak, J. Strejcek, and L. Helouet: Decidable Race Condition for HMSC, FI MU Report Series, FIMU-RS-2009-10, 2009. [PDF]

  3. L. Bozzelli, M. Kretinsky, V. Rehak, and J. Strejcek: 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]

  4. A. Bouajjani, J. Strejcek, 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]

  5. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek: 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]

  6. M. Kretinsky, V. Rehak, and J. Strejcek: Refining the Undecidability Border of Weak Bisimilarity, FI MU Report Series, FIMU-RS-2005-06, 2005. Full version of INFINITY'05 paper. [postscript]

  7. A. Kucera and J. Strejcek: Characteristic Patterns for LTL, FI MU Report Series, FIMU-RS-2004-10, 2004. Full version of SOFSEM'05 paper. [postscript]

  8. R. Pelanek and J. Strejcek: Deeper Connections between LTL and Alternating Automata, FI MU Report Series, FIMU-RS-2004-08, 2004. [postscript]

  9. A. Kucera and J. Strejcek: 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]

  10. M. Kretinsky, V. Rehak, and J. Strejcek: On the Expressive Power of Extended Process Rewrite Systems, Technical Report RS-04-07, Basic Research in Computer Science, Aarhus, Denmark, 2004. [postscript]

  11. M. Kretinsky, V. Rehak, and J. Strejcek: Process Rewrite Systems with Weak Finite-State Unit, FI MU Report Series, FIMU-RS-2003-05, 2003. Full version of INFINITY'03 paper. [postscript]

  12. A. Kucera and J. Strejcek: 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]

  13. J. Strejcek: 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