| 2026 | TACAS | Symbiotic 11 Predicate Abstraction Joins the Party - (Competition Contribution). | Paulna Ayaziov, Martin Jons, Vincent Mihalkovic, Jindrich Sedlcek, Jan Strejcek |
| 2026 | TACAS | Evaluating Software Verifiers for C, Java, and SV-LIB - (Report on SV-COMP 2026). | Dirk Beyer, Jan Strejcek |
| 2026 | TACAS | Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses - (Competition Contribution). | Karoliine Holter, Paulna Ayaziov, Simmo Saan, Jan Strejcek, Vesal Vojdani |
| 2026 | TACAS | Re3ver: Reverse and Verify - (Competition Contribution). | Adla Stepkov, Martin Jons, Jan Strejcek |
| 2025 | FASE | Fizzer with Local Space Fuzzing - (Competition Contribution). | Martin Jons, Jan Strejcek, Marek Trtk |
| 2025 | FCT | On Complementation of Nondeterministic Finite Automata Without Full Determinization. | Luks Holk, Ondrej Lengl, Juraj Major, Adla Stepkov, Jan Strejcek |
| 2025 | TACAS | Improvements in Software Verification and Witness Validation: SV-COMP 2025. | Dirk Beyer, Jan Strejcek |
| 2024 | FASE | Fizzer: New Gray-Box Fuzzer - (Competition Contribution). | Martin Jons, Jan Strejcek, Marek Trtk, Luks Urban |
| 2024 | FMCAD | Combining Symbolic Execution with Predicate Abstraction and CEGAR. | Martin Jons, Jan Strejcek, Alberto Griggio |
| 2024 | FOSSACS | Tighter Construction of Tight Bchi Automata. | Marek Jankola, Jan Strejcek |
| 2024 | TACAS | Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution). | Paulna Ayaziov, Jan Strejcek |
| 2024 | TACAS | Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution - (Competition Contribution). | Martin Jons, Kristin Kumor, Jakub Novk, Jindrich Sedlcek, Marek Trtk, Luks Zaoral, Paulna Ayaziov, Jan Strejcek |
| 2024 | TACAS | Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. | Martin Jons, Jan Strejcek, Marek Trtk, Luks Urban |
| 2023 | SAT | Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. | Tereza Schwarzov, Jan Strejcek, Juraj Major |
| 2023 | TACAS | Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution). | Paulna Ayaziov, Jan Strejcek |
| 2022 | SAS | Case Study on Verification-Witness Validators: Where We Are and Where We Go. | Dirk Beyer, Jan Strejcek |
| 2022 | TACAS | Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution). | Paulna Ayaziov, Marek Chalupa, Jan Strejcek |
| 2022 | TACAS | Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution). | Marek Chalupa, Vincent Mihalkovic, Anna Rechtckov, Luks Zaoral, Jan Strejcek |
| 2021 | CAV | Fast Computation of Strong Control Dependencies. | Marek Chalupa, David Klaska, Jan Strejcek, Luks Tomovic |
| 2021 | FASE | Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution). | Marek Chalupa, Jakub Novk, Jan Strejcek |
| 2021 | SAS | Backward Symbolic Execution with Loop Folding. | Marek Chalupa, Jan Strejcek |
| 2021 | SAT | DQBDD: An Efficient BDD-Based DQBF Solver. | Juraj Sc, Jan Strejcek |
| 2021 | TACAS | Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution). | Marek Chalupa, Toms Jasek, Jakub Novk, Anna Rechtckov, Veronika Sokov, Jan Strejcek |
| 2020 | CAV | Seminator 2 Can Complement Generalized Bchi Automata via Improved Semi-determinization. | Frantisek Blahoudek, Alexandre Duret-Lutz, Jan Strejcek |
| 2020 | SAT | Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. | Martin Jons, Jan Strejcek |
| 2020 | TACAS | Symbiotic 7: Integration of Predator and More - (Competition Contribution). | Marek Chalupa, Toms Jasek, Luks Tomovic, Martin Hruska, Veronika Sokov, Paulna Ayaziov, Jan Strejcek, Toms Vojnar |
| 2019 | ATVA | Generic Emptiness Check for Fun and Profit. | Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Mller, Jan Strejcek |
| 2019 | ATVA | ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. | Juraj Major, Frantisek Blahoudek, Jan Strejcek, Miriama Sasarkov, Tatiana Zbonckov |
| 2019 | CAV | Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. | Martin Jons, Jan Strejcek |
| 2019 | ICTAC | LTL to Smaller Self-Loop Alternating Automata and Back. | Frantisek Blahoudek, Juraj Major, Jan Strejcek |
| 2019 | IFM | Evaluation of Program Slicing in Software Verification. | Marek Chalupa, Jan Strejcek |
| 2018 | ICTAC | Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. | Martin Jons, Jan Strejcek |
| 2018 | LPAR | Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper). | Martin Jons, Jan Strejcek |
| 2018 | TACAS | SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution). | Marek Chalupa, Martina Vitovsk, Jan Strejcek |
| 2017 | LPAR | Seminator: A Tool for Semi-Determinization of Omega-Automata. | Frantisek Blahoudek, Alexandre Duret-Lutz, Mikuls Klokocka, Mojmr Kretnsk, Jan Strejcek |
| 2017 | SAT | On Simplification of Formulas with Unconstrained Variables and Quantifiers. | Martin Jons, Jan Strejcek |
| 2017 | TACAS | Symbiotic 4: Beyond Reachability - (Competition Contribution). | Marek Chalupa, Martina Vitovsk, Martin Jons, Jiri Slaby, Jan Strejcek |
| 2016 | ATVA | Tighter Loop Bound Analysis. | Pavel Cadek, Jan Strejcek, Marek Trtk |
| 2016 | SAT | Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. | Martin Jons, Jan Strejcek |
| 2016 | TACAS | Complementing Semi-deterministic Bchi Automata. | Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai |
| 2016 | TACAS | Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). | Marek Chalupa, Martin Jons, Jiri Slaby, Jan Strejcek, Martina Vitovsk |
| 2015 | CAV | The Hanoi Omega-Automata Format. | Toms Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretnsk, David Mller, David Parker, Jan Strejcek |
| 2014 | ATVA | Symbolic Memory with Pointers. | Marek Trtk, Jan Strejcek |
| 2014 | TACAS | Symbiotic 2: More Precise Slicing - (Competition Contribution). | Jiri Slaby, Jan Strejcek |
| 2013 | ATVA | Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. | Toms Babiak, Frantisek Blahoudek, Mojmr Kretnsk, Jan Strejcek |
| 2013 | ATVA | Compact Symbolic Execution. | Jiri Slaby, Jan Strejcek, Marek Trtk |
| 2013 | LPAR | Comparison of LTL to Deterministic Rabin Automata Translators. | Frantisek Blahoudek, Mojmr Kretnsk, Jan Strejcek |
| 2013 | TACAS | Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). | Jiri Slaby, Jan Strejcek, Marek Trtk |
| 2013 | VMCAI | ClabureDB: Classified Bug-Reports Database. | Jiri Slaby, Jan Strejcek, Marek Trtk |
| 2012 | FMICS | Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. | Jiri Slaby, Jan Strejcek, Marek Trtk |
| 2012 | ISSTA | Abstracting path conditions. | Jan Strejcek, Marek Trtk |
| 2012 | TACAS | LTL to Bchi Automata Translation: Fast and More Deterministic. | Toms Babiak, Mojmr Kretnsk, Vojtech Rehk, Jan Strejcek |
| 2005 | SOFSEM | Characteristic Patterns for LTL. | Antonn Kucera, Jan Strejcek |
| 2004 | CONCUR | Extended Process Rewrite Systems: Expressiveness and Reachability. | Mojmr Kretnsk, Vojtech Rehk, Jan Strejcek |
| 2002 | CSL | The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. | Antonn Kucera, Jan Strejcek |