Jan Strejcek

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 45

Top Topics

Deterministic Automata

Top Venues

Publications

Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban
Fizzer: New Gray-Box Fuzzer - (Competition Contribution). FASE (2024)
Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. TACAS (3) (2024)
Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage (Technical Report). CoRR (2024)
Martin Jonás, Kristián Kumor, Jakub Novák, Jindrich Sedlácek, Marek Trtík, Lukás Zaoral, Paulína Ayaziová, Jan Strejcek
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution - (Competition Contribution). TACAS (3) (2024)
Martin Jonás, Jan Strejcek
Truncating abstraction of bit-vector operations for BDD-based SMT solvers. Theor. Comput. Sci. 1008 (2024)
Marek Jankola, Jan Strejcek
Tighter Construction of Tight Büchi Automata. FoSSaCS (1) (2024)
Paulína Ayaziová, Jan Strejcek
Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution). TACAS (3) (2024)
Paulína Ayaziová, Jan Strejcek
Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution). TACAS (2) (2023)
Tereza Schwarzová, Jan Strejcek, Juraj Major
Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. SAT (2023)
Paulína Ayaziová, Marek Chalupa, Jan Strejcek
Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution). TACAS (2) (2022)
Marek Chalupa, Vincent Mihalkovic, Anna Rechtácková, Lukás Zaoral, Jan Strejcek
Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution). TACAS (2) (2022)
Dirk Beyer, Jan Strejcek
Case Study on Verification-Witness Validators: Where We Are and Where We Go. SAS (2022)
Marek Chalupa, Tomás Jasek, Jakub Novák, Anna Rechtácková, Veronika Soková, Jan Strejcek
Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution). TACAS (2) (2021)
Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic
Fast Computation of Strong Control Dependencies. CAV (2) (2021)
Juraj Síc, Jan Strejcek
DQBDD: An Efficient BDD-Based DQBF Solver. SAT (2021)
Marek Chalupa, Jan Strejcek
Backward Symbolic Execution with Loop Folding. SAS (2021)
Marek Chalupa, Martina Vitovská, Tomás Jasek, Michael Simácek, Jan Strejcek
Symbiotic 6: generating test cases by slicing and symbolic execution. Int. J. Softw. Tools Technol. Transf. 23 (6) (2021)
Marek Chalupa, Jakub Novák, Jan Strejcek
Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution). FASE (2021)
Marek Chalupa, Jan Strejcek, Martina Vitovská
Joint forces for memory safety checking revisited. Int. J. Softw. Tools Technol. Transf. 22 (2) (2020)
Marek Chalupa, Tomás Jasek, Lukás Tomovic, Martin Hruska, Veronika Soková, Paulína Ayaziová, Jan Strejcek, Tomás Vojnar
Symbiotic 7: Integration of Predator and More - (Competition Contribution). TACAS (2) (2020)
Frantisek Blahoudek, Juraj Major, Jan Strejcek
LTL to self-loop alternating automata with generic acceptance and back. Theor. Comput. Sci. 840 (2020)
Frantisek Blahoudek, Alexandre Duret-Lutz, Jan Strejcek
Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. CAV (2) (2020)
Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic
Fast Computation of Strong Control Dependencies. CoRR (2020)
Martin Jonás, Jan Strejcek
Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. SAT (2020)
Marek Chalupa, Jan Strejcek
Evaluation of Program Slicing in Software Verification. IFM (2019)
Martin Jonás, Jan Strejcek
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. CAV (2) (2019)
Frantisek Blahoudek, Juraj Major, Jan Strejcek
LTL to Smaller Self-Loop Alternating Automata and Back. CoRR (2019)
Frantisek Blahoudek, Juraj Major, Jan Strejcek
LTL to Smaller Self-Loop Alternating Automata and Back. ICTAC (2019)
Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, Jan Strejcek
Generic Emptiness Check for Fun and Profit. ATVA (2019)
Juraj Major, Frantisek Blahoudek, Jan Strejcek, Miriama Sasaráková, Tatiana Zboncáková
ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. ATVA (2019)
Marek Chalupa, Martina Vitovská, Jan Strejcek
SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution). TACAS (2) (2018)
Martina Vitovská, Marek Chalupa, Jan Strejcek
SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode. CoRR (2018)
Martin Jonás, Jan Strejcek
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper). LPAR (2018)
Marek Chalupa, Jan Strejcek, Martina Vitovská
Joint Forces for Memory Safety Checking. SPIN (2018)
Martin Jonás, Jan Strejcek
Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. ICTAC (2018)
Martin Jonás, Jan Strejcek
On the complexity of the quantified bit-vector arithmetic with binary encoding. Inf. Process. Lett. 135 (2018)
Frantisek Blahoudek, Alexandre Duret-Lutz, Mikulás Klokocka, Mojmír Kretínský, Jan Strejcek
Seminator: A Tool for Semi-Determinization of Omega-Automata. LPAR (2017)
Marek Chalupa, Martina Vitovská, Martin Jonás, Jiri Slaby, Jan Strejcek
Symbiotic 4: Beyond Reachability - (Competition Contribution). TACAS (2) (2017)
Martin Jonás, Jan Strejcek
On Simplification of Formulas with Unconstrained Variables and Quantifiers. SAT (2017)
Pavel Cadek, Jan Strejcek, Marek Trtík
Tighter Loop Bound Analysis (Technical report). CoRR (2016)
Martin Jonás, Jan Strejcek
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. SAT (2016)
Pavel Cadek, Jan Strejcek, Marek Trtík
Tighter Loop Bound Analysis. ATVA (2016)
Martin Jonás, Jan Strejcek
On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoded Bit-Widths. CoRR (2016)
Marek Chalupa, Martin Jonás, Jiri Slaby, Jan Strejcek, Martina Vitovská
Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). TACAS (2016)
Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai
Complementing Semi-deterministic Büchi Automata. TACAS (2016)
Frantisek Blahoudek, Alexandre Duret-Lutz, Vojtech Rujbr, Jan Strejcek
On Refinement of Büchi Automata for Explicit Model Checking. SPIN (2015)
Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretínský, David Müller, David Parker, Jan Strejcek
The Hanoi Omega-Automata Format. CAV (1) (2015)
Jiri Slaby, Jan Strejcek
Symbiotic 2: More Precise Slicing - (Competition Contribution). TACAS (2014)
Frantisek Blahoudek, Alexandre Duret-Lutz, Mojmír Kretínský, Jan Strejcek
Is there a best büchi automaton for explicit model checking? SPIN (2014)
Marek Trtík, Jan Strejcek
Symbolic Memory with Pointers. ATVA (2014)
Tomás Babiak, Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. ATVA (2013)
Jiri Slaby, Jan Strejcek, Marek Trtík
Compact Symbolic Execution. ATVA (2013)
Jiri Slaby, Jan Strejcek, Marek Trtík
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). TACAS (2013)
Tomás Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Kretínský, Jan Strejcek
Compositional Approach to Suspension and Other Improvements to LTL Translation. SPIN (2013)
Jiri Slaby, Jan Strejcek, Marek Trtík
ClabureDB: Classified Bug-Reports Database. VMCAI (2013)
Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek
Comparison of LTL to Deterministic Rabin Automata Translators. LPAR (2013)
Tomás Babiak, Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment. CoRR (2013)
Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
LTL to Büchi Automata Translation: Fast and More Deterministic CoRR (2012)
Tomás Babiak, Vojtech Rehák, Jan Strejcek
Almost linear Büchi automata. Math. Struct. Comput. Sci. 22 (2) (2012)
Jan Strejcek, Marek Trtík
Abstracting path conditions. ISSTA (2012)
Jiri Slaby, Jan Strejcek, Marek Trtík
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. FMICS (2012)
Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
LTL to Büchi Automata Translation: Fast and More Deterministic. TACAS (2012)
Jiri Slaby, Jan Strejcek, Marek Trtík
On Synergy of Metal, Slicing, and Symbolic Execution CoRR (2012)
Jan Strejcek, Marek Trtík
Abstracting Path Conditions CoRR (2011)
Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness CoRR (2010)
Vojtech Rehák, Petr Slovák, Jan Strejcek, Loïc Hélouët
Decidable Race Condition and Open Coregions in HMSC. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 29 (2010)
Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
On decidability of LTL model checking for process rewrite systems. Acta Informatica 46 (1) (2009)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
On Decidability of LTL+Past Model Checking for Process Rewrite Systems. INFINITY (2009)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
Reachability is decidable for weakly extended process rewrite systems. Inf. Comput. 207 (6) (2009)
Tomás Babiak, Vojtech Rehák, Jan Strejcek
Almost Linear Büchi Automata EXPRESS (2009)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
Petri nets are less expressive than state-extended PA. Theor. Comput. Sci. 394 (1-2) (2008)
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek
Reachability analysis of multithreaded software with asynchronous communication. Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)
Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
On Decidability of LTL Model Checking for Process Rewrite Systems. FSTTCS (2006)
Ahmed Bouajjani, Jan Strejcek, Tayssir Touili
On Symbolic Verification of Weakly Extended PAD. EXPRESS (2006)
Antonín Kucera, Jan Strejcek
The stuttering principle revisited. Acta Informatica 41 (7-8) (2005)
Antonín Kucera, Jan Strejcek
Characteristic Patterns for LTL. SOFSEM (2005)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
Refining the Undecidability Border of Weak Bisimilarity. INFINITY (2005)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
Reachability of Hennessy-Milner Properties for Weakly Extended PRS. FSTTCS (2005)
Radek Pelánek, Jan Strejcek
Deeper Connections Between LTL and Alternating Automata. CIAA (2005)
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek
Reachability Analysis of Multithreaded Software with Asynchronous Communication. FSTTCS (2005)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
Extended Process Rewrite Systems: Expressiveness and Reachability. CONCUR (2004)
Mojmír Kretínský, Vojtech Rehák, Jan Strejcek
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. INFINITY (2003)
Antonín Kucera, Jan Strejcek
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. CSL (2002)
Jan Strejcek
Rewrite Systems with Constraints. EXPRESS (2001)