Rewrite Systems with Constraints. - Jan Strejcek (EXPRESS, 2001)

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. - Antonín Kucera 001; Jan Strejcek (CSL, 2002)

On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (INFINITY, 2003)

Extended Process Rewrite Systems: Expressiveness and Reachability. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (CONCUR, 2004)

Reachability of Hennessy-Milner Properties for Weakly Extended PRS. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (FSTTCS, 2005)

Characteristic Patterns for LTL. - Antonín Kucera 001; Jan Strejcek (SOFSEM, 2005)

Deeper Connections Between LTL and Alternating Automata. - Radek Pelánek; Jan Strejcek (CIAA, 2005)

The stuttering principle revisited. - Antonín Kucera 001; Jan Strejcek (Acta Informatica, 2005)

Refining the Undecidability Border of Weak Bisimilarity. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (INFINITY, 2005)

Reachability analysis of multithreaded software with asynchronous communication. - Ahmed Bouajjani; Javier Esparza; Stefan Schwoon; Jan Strejcek (Software Verification: Infinite-State Model Checking and Static Program Analysis, 2006)

On Symbolic Verification of Weakly Extended PAD. - Ahmed Bouajjani; Jan Strejcek; Tayssir Touili (EXPRESS, 2006)

Petri nets are less expressive than state-extended PA. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (Theor. Comput. Sci., 2008)

On decidability of LTL model checking for process rewrite systems. - Laura Bozzelli; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (Acta Informatica, 2009)

Almost Linear Büchi Automata - Tomás Babiak; Vojtech Rehák; Jan Strejcek (EXPRESS, 2009)

On Decidability of LTL+Past Model Checking for Process Rewrite Systems. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (INFINITY, 2009)

Reachability is decidable for weakly extended process rewrite systems. - Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (Inf. Comput., 2009)

A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness - Tomás Babiak; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (CoRR, 2010)

Decidable Race Condition and Open Coregions in HMSC. - Vojtech Rehák; Petr Slovák; Jan Strejcek; Loïc Hélouët (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010)

Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. - Jiri Slaby; Jan Strejcek; Marek Trtík (FMICS, 2012)

Abstracting path conditions. - Jan Strejcek; Marek Trtík (ISSTA, 2012)

LTL to Büchi Automata Translation: Fast and More Deterministic. - Tomás Babiak; Mojmír Kretínský; Vojtech Rehák; Jan Strejcek (TACAS, 2012)

On Synergy of Metal, Slicing, and Symbolic Execution - Jiri Slaby; Jan Strejcek; Marek Trtík (CoRR, 2012)

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. - Tomás Babiak; Frantisek Blahoudek; Mojmír Kretínský; Jan Strejcek (ATVA, 2013)

Compact Symbolic Execution. - Jiri Slaby; Jan Strejcek; Marek Trtík (ATVA, 2013)

Comparison of LTL to Deterministic Rabin Automata Translators. - Frantisek Blahoudek; Mojmír Kretínský; Jan Strejcek (LPAR, 2013)

Compositional Approach to Suspension and Other Improvements to LTL Translation. - Tomás Babiak; Thomas Badie; Alexandre Duret-Lutz; Mojmír Kretínský; Jan Strejcek (SPIN, 2013)

Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). - Jiri Slaby; Jan Strejcek; Marek Trtík (TACAS, 2013)

ClabureDB: Classified Bug-Reports Database. - Jiri Slaby; Jan Strejcek; Marek Trtík (VMCAI, 2013)

Symbolic Memory with Pointers. - Marek Trtík; Jan Strejcek (ATVA, 2014)

Is there a best büchi automaton for explicit model checking? - Frantisek Blahoudek; Alexandre Duret-Lutz; Mojmír Kretínský; Jan Strejcek (SPIN, 2014)

Symbiotic 2: More Precise Slicing - (Competition Contribution). - Jiri Slaby; Jan Strejcek (TACAS, 2014)

The Hanoi Omega-Automata Format. - Tomás Babiak; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; Jan Kretínský; David Müller 001; David Parker 001; Jan Strejcek (CAV (1), 2015)

On Refinement of Büchi Automata for Explicit Model Checking. - Frantisek Blahoudek; Alexandre Duret-Lutz; Vojtech Rujbr; Jan Strejcek (SPIN, 2015)

Tighter Loop Bound Analysis. - Pavel Cadek; Jan Strejcek; Marek Trtík (ATVA, 2016)

Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. - Martin Jonás; Jan Strejcek (SAT, 2016)

Complementing Semi-deterministic Büchi Automata. - Frantisek Blahoudek; Matthias Heizmann; Sven Schewe; Jan Strejcek; Ming-Hsien Tsai 001 (TACAS, 2016)

Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). - Marek Chalupa; Martin Jonás; Jiri Slaby; Jan Strejcek; Martina Vitovská (TACAS, 2016)

Tighter Loop Bound Analysis (Technical report). - Pavel Cadek; Jan Strejcek; Marek Trtík (CoRR, 2016)

On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoded Bit-Widths. - Martin Jonás; Jan Strejcek (CoRR, 2016)

Seminator: A Tool for Semi-Determinization of Omega-Automata. - Frantisek Blahoudek; Alexandre Duret-Lutz; Mikulás Klokocka; Mojmír Kretínský; Jan Strejcek (LPAR, 2017)

On Simplification of Formulas with Unconstrained Variables and Quantifiers. - Martin Jonás; Jan Strejcek (SAT, 2017)

Symbiotic 4: Beyond Reachability - (Competition Contribution). - Marek Chalupa; Martina Vitovská; Martin Jonás; Jiri Slaby; Jan Strejcek (TACAS (2), 2017)

Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. - Martin Jonás; Jan Strejcek (ICTAC, 2018)

Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper). - Martin Jonás; Jan Strejcek (LPAR, 2018)

Joint Forces for Memory Safety Checking. - Marek Chalupa; Jan Strejcek; Martina Vitovská (SPIN, 2018)

SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution). - Marek Chalupa; Martina Vitovská; Jan Strejcek (TACAS (2), 2018)

SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode. - Martina Vitovská; Marek Chalupa; Jan Strejcek (CoRR, 2018)

On the complexity of the quantified bit-vector arithmetic with binary encoding. - Martin Jonás; Jan Strejcek (Inf. Process. Lett., 2018)

Generic Emptiness Check for Fun and Profit. - Christel Baier; Frantisek Blahoudek; Alexandre Duret-Lutz; Joachim Klein 001; David Müller 001; Jan Strejcek (ATVA, 2019)

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. - Juraj Major; Frantisek Blahoudek; Jan Strejcek; Miriama Sasaráková; Tatiana Zboncáková (ATVA, 2019)

Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. - Martin Jonás; Jan Strejcek (CAV (2), 2019)

LTL to Smaller Self-Loop Alternating Automata and Back. - Frantisek Blahoudek; Juraj Major; Jan Strejcek (ICTAC, 2019)

Evaluation of Program Slicing in Software Verification. - Marek Chalupa; Jan Strejcek (IFM, 2019)

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. - Frantisek Blahoudek; Alexandre Duret-Lutz; Jan Strejcek (CAV (2), 2020)

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. - Martin Jonás; Jan Strejcek (SAT, 2020)

Symbiotic 7: Integration of Predator and More - (Competition Contribution). - Marek Chalupa; Tomás Jasek; Lukás Tomovic; Martin Hruska; Veronika Soková; Paulína Ayaziová; Jan Strejcek; Tomás Vojnar (TACAS (2), 2020)

Joint forces for memory safety checking revisited. - Marek Chalupa; Jan Strejcek; Martina Vitovská (Int. J. Softw. Tools Technol. Transf., 2020)

LTL to self-loop alternating automata with generic acceptance and back. - Frantisek Blahoudek; Juraj Major; Jan Strejcek (Theor. Comput. Sci., 2020)

Fast Computation of Strong Control Dependencies. - Marek Chalupa; David Klaska; Jan Strejcek; Lukás Tomovic (CAV (2), 2021)

Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution). - Marek Chalupa; Jakub Novák; Jan Strejcek (FASE, 2021)

Backward Symbolic Execution with Loop Folding. - Marek Chalupa; Jan Strejcek (SAS, 2021)

DQBDD: An Efficient BDD-Based DQBF Solver. - Juraj Síc; Jan Strejcek (SAT, 2021)

Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution). - Marek Chalupa; Tomás Jasek; Jakub Novák; Anna Rechtácková; Veronika Soková; Jan Strejcek (TACAS (2), 2021)

Symbiotic 6: generating test cases by slicing and symbolic execution. - Marek Chalupa; Martina Vitovská; Tomás Jasek; Michael Simácek; Jan Strejcek (Int. J. Softw. Tools Technol. Transf., 2021)

Case Study on Verification-Witness Validators: Where We Are and Where We Go. - Dirk Beyer 001; Jan Strejcek (SAS, 2022)

Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution). - Paulína Ayaziová; Marek Chalupa; Jan Strejcek (TACAS (2), 2022)

Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution). - Marek Chalupa; Vincent Mihalkovic; Anna Rechtácková; Lukás Zaoral; Jan Strejcek (TACAS (2), 2022)

Reproduction Package for SAS 2022 Article 'Case Study on Verification-Witness Validators: Where We Are and Where We Go'. - Dirk Beyer 001; Jan Strejcek (Zenodo, 2022)

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. - Tereza Schwarzová; Jan Strejcek; Juraj Major (SAT, 2023)

Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution). - Paulína Ayaziová; Jan Strejcek (TACAS (2), 2023)

Reproduction Package for FSE 2024 Submission 'Verification Witnesses Version 2'. - Paulína Ayaziová; Dirk Beyer 001; Marian Lingsch Rosenfeld; Martin Spiessl; Jan Strejcek (Zenodo, 2023)

Fizzer: New Gray-Box Fuzzer - (Competition Contribution). - Martin Jonás; Jan Strejcek; Marek Trtík; Lukás Urban (FASE, 2024)

Combining Symbolic Execution with Predicate Abstraction and CEGAR. - Martin Jonás; Jan Strejcek; Alberto Griggio (FMCAD, 2024)

Tighter Construction of Tight Büchi Automata. - Marek Jankola; Jan Strejcek (FoSSaCS (1), 2024)

Software Verification Witnesses 2.0. - Paulína Ayaziová; Dirk Beyer 001; Marian Lingsch Rosenfeld; Martin Spiessl; Jan Strejcek (SPIN, 2024)

Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution). - Paulína Ayaziová; Jan Strejcek (TACAS (3), 2024)

Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution - (Competition Contribution). - Martin Jonás; Kristián Kumor; Jakub Novák; Jindrich Sedlácek; Marek Trtík; Lukás Zaoral; Paulína Ayaziová; Jan Strejcek (TACAS (3), 2024)

Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. - Martin Jonás; Jan Strejcek; Marek Trtík; Lukás Urban (TACAS (3), 2024)

Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage (Technical Report). - Martin Jonás; Jan Strejcek; Marek Trtík; Lukás Urban (CoRR, 2024)

Truncating abstraction of bit-vector operations for BDD-based SMT solvers. - Martin Jonás; Jan Strejcek (Theor. Comput. Sci., 2024)

Reproduction Package for SPIN 2024 Submission 'Verification Witnesses Version 2'. - Paulína Ayaziová; Dirk Beyer 001; Marian Lingsch Rosenfeld; Martin Spiessl; Jan Strejcek (Zenodo, 2024)

Reproduction Package for SPIN 2024 Submission 'Verification Witnesses Version 2'. - Paulína Ayaziová; Dirk Beyer 001; Marian Lingsch Rosenfeld; Martin Spiessl; Jan Strejcek (Zenodo, 2024)

Reproduction Package for SPIN 2024 Article 'Verification Witnesses Version 2'. - Paulína Ayaziová; Dirk Beyer 001; Marian Lingsch Rosenfeld; Martin Spiessl; Jan Strejcek (Zenodo, 2024)

Fizzer with Local Space Fuzzing - (Competition Contribution). - Martin Jonás; Jan Strejcek; Marek Trtík (FASE, 2025)

Improvements in Software Verification and Witness Validation: SV-COMP 2025. - Dirk Beyer 001; Jan Strejcek (TACAS (3), 2025)

Gray-Box Fuzzing in Local Space. - Martin Jonás; Jan Strejcek; Marek Trtík (CoRR, 2025)

On Complementation of Nondeterministic Finite Automata without Full Determinization (Technical Report). - Lukás Holík; Ondrej Lengál; Juraj Major; Adéla Stepková; Jan Strejcek (CoRR, 2025)