Jan Strejcek

According to our database, Jan Strejcek authored at least 79 papers between 2001 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Truncating abstraction of bit-vector operations for BDD-based SMT solvers.

Martin Jonás, Jan Strejcek

Theor. Comput. Sci., 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

Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage.

Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution).

Paulína Ayaziová, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Software Verification Witnesses 2.0.

Paulína Ayaziová, Dirk Beyer, Marian Lingsch Rosenfeld, Martin Spiessl, Jan Strejcek

Proceedings of the Model Checking Software - 30th International Symposium, 2024

Tighter Construction of Tight Büchi Automata.

Marek Jankola, Jan Strejcek

Proceedings of the Foundations of Software Science and Computation Structures, 2024

Fizzer: New Gray-Box Fuzzer - (Competition Contribution).

Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban

Proceedings of the Fundamental Approaches to Software Engineering, 2024

2023

Reproduction Package for FSE 2024 Submission 'Verification Witnesses Version 2'.

Paulína Ayaziová, Dirk Beyer, Marian Lingsch Rosenfeld, Martin Spiessl, Jan Strejcek

Dataset, October, 2023

Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution).

Paulína Ayaziová, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving.

Tereza Schwarzová, Jan Strejcek, Juraj Major

Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

2022

Reproduction Package for SAS 2022 Article 'Case Study on Verification-Witness Validators: Where We Are and Where We Go'.

Dirk Beyer, Jan Strejcek

Dataset, January, 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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution).

Paulína Ayaziová, Marek Chalupa, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Case Study on Verification-Witness Validators: Where We Are and Where We Go.

Dirk Beyer, Jan Strejcek

Proceedings of the Static Analysis - 29th International Symposium, 2022

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

Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution).

Marek Chalupa, Tomás Jasek, Jakub Novák, Anna Rechtácková, Veronika Soková, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

DQBDD: An Efficient BDD-Based DQBF Solver.

Juraj Síc, Jan Strejcek

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Backward Symbolic Execution with Loop Folding.

Marek Chalupa, Jan Strejcek

Proceedings of the Static Analysis - 28th International Symposium, 2021

Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution).

Marek Chalupa, Jakub Novák, Jan Strejcek

Proceedings of the Fundamental Approaches to Software Engineering, 2021

Fast Computation of Strong Control Dependencies.

Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

LTL to self-loop alternating automata with generic acceptance and back.

Frantisek Blahoudek, Juraj Major, Jan Strejcek

Theor. Comput. Sci., 2020

Joint forces for memory safety checking revisited.

Marek Chalupa, Jan Strejcek, Martina Vitovská

Int. J. Softw. Tools Technol. Transf., 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

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions.

Martin Jonás, Jan Strejcek

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization.

Frantisek Blahoudek, Alexandre Duret-Lutz, Jan Strejcek

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Evaluation of Program Slicing in Software Verification.

Marek Chalupa, Jan Strejcek

Proceedings of the Integrated Formal Methods - 15th International Conference, 2019

LTL to Smaller Self-Loop Alternating Automata and Back.

Frantisek Blahoudek, Juraj Major, Jan Strejcek

Proceedings of the Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31, 2019

Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors.

Martin Jonás, Jan Strejcek

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata.

Juraj Major, Frantisek Blahoudek, Jan Strejcek, Miriama Sasaráková, Tatiana Zboncáková

Proceedings of the Automated Technology for Verification and Analysis, 2019

Generic Emptiness Check for Fun and Profit.

Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, Jan Strejcek

Proceedings of the Automated Technology for Verification and Analysis, 2019

2018

On the complexity of the quantified bit-vector arithmetic with binary encoding.

Martin Jonás, Jan Strejcek

Inf. Process. Lett., 2018

SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode.

Martina Vitovská, Marek Chalupa, Jan Strejcek

CoRR, 2018

SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution).

Marek Chalupa, Martina Vitovská, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Joint Forces for Memory Safety Checking.

Marek Chalupa, Jan Strejcek, Martina Vitovská

Proceedings of the Model Checking Software - 25th International Symposium, 2018

Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper).

Martin Jonás, Jan Strejcek

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers.

Martin Jonás, Jan Strejcek

Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

2017

Symbiotic 4: Beyond Reachability - (Competition Contribution).

Marek Chalupa, Martina Vitovská, Martin Jonás, Jiri Slaby, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

On Simplification of Formulas with Unconstrained Variables and Quantifiers.

Martin Jonás, Jan Strejcek

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28, 2017

Seminator: A Tool for Semi-Determinization of Omega-Automata.

Frantisek Blahoudek, Alexandre Duret-Lutz, Mikulás Klokocka, Mojmír Kretínský, Jan Strejcek

Proceedings of the LPAR-21, 2017

2016

On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoded Bit-Widths.

Martin Jonás, Jan Strejcek

CoRR, 2016

Tighter Loop Bound Analysis (Technical report).

Pavel Cadek, Jan Strejcek, Marek Trtík

CoRR, 2016

Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution).

Marek Chalupa, Martin Jonás, Jiri Slaby, Jan Strejcek, Martina Vitovská

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Complementing Semi-deterministic Büchi Automata.

Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams.

Martin Jonás, Jan Strejcek

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Tighter Loop Bound Analysis.

Pavel Cadek, Jan Strejcek, Marek Trtík

Proceedings of the Automated Technology for Verification and Analysis, 2016

2015

On Refinement of Büchi Automata for Explicit Model Checking.

Frantisek Blahoudek, Alexandre Duret-Lutz, Vojtech Rujbr, Jan Strejcek

Proceedings of the Model Checking Software - 22nd International Symposium, 2015

The Hanoi Omega-Automata Format.

Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretínský, David Müller, David Parker, Jan Strejcek

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014

Symbiotic 2: More Precise Slicing - (Competition Contribution).

Jiri Slaby, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Is there a best büchi automaton for explicit model checking?

Frantisek Blahoudek, Alexandre Duret-Lutz, Mojmír Kretínský, Jan Strejcek

Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

Symbolic Memory with Pointers.

Marek Trtík, Jan Strejcek

Proceedings of the Automated Technology for Verification and Analysis, 2014

2013

ClabureDB: Classified Bug-Reports Database.

Jiri Slaby, Jan Strejcek, Marek Trtík

Proceedings of the Verification, 2013

Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution).

Jiri Slaby, Jan Strejcek, Marek Trtík

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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

Proceedings of the Model Checking Software - 20th International Symposium, 2013

Comparison of LTL to Deterministic Rabin Automata Translators.

Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Compact Symbolic Execution.

Jiri Slaby, Jan Strejcek, Marek Trtík

Proceedings of the Automated Technology for Verification and Analysis, 2013

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment.

Tomás Babiak, Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

On Synergy of Metal, Slicing, and Symbolic Execution

Jiri Slaby, Jan Strejcek, Marek Trtík

CoRR, 2012

LTL to Büchi Automata Translation: Fast and More Deterministic.

Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Abstracting path conditions.

Jan Strejcek, Marek Trtík

Proceedings of the International Symposium on Software Testing and Analysis, 2012

Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution.

Jiri Slaby, Jan Strejcek, Marek Trtík

Proceedings of the Formal Methods for Industrial Critical Systems, 2012

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

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

2009

Reachability is decidable for weakly extended process rewrite systems.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Inf. Comput., 2009

On Decidability of LTL+Past Model Checking for Process Rewrite Systems.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Proceedings of the Joint Proceedings of the 8th, 2009

Almost Linear Büchi Automata

Tomás Babiak, Vojtech Rehák, Jan Strejcek

Proceedings of the Proceedings 16th International Workshop on Expressiveness in Concurrency, 2009

On decidability of LTL model checking for process rewrite systems.

Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Acta Informatica, 2009

2008

Petri nets are less expressive than state-extended PA.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Theor. Comput. Sci., 2008

2006

On Symbolic Verification of Weakly Extended PAD.

Ahmed Bouajjani, Jan Strejcek, Tayssir Touili

Proceedings of the 13th International Workshop on Expressiveness in Concurrency, 2006

Reachability analysis of multithreaded software with asynchronous communication.

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek

Proceedings of the Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02., 2006

2005

Refining the Undecidability Border of Weak Bisimilarity.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Proceedings of the 7th International Workshop on Verification of Infinite-State Systems, 2005

The stuttering principle revisited.

Antonín Kucera, Jan Strejcek

Acta Informatica, 2005

Deeper Connections Between LTL and Alternating Automata.

Radek Pelánek, Jan Strejcek

Proceedings of the Implementation and Application of Automata, 2005

Characteristic Patterns for LTL.

Antonín Kucera, Jan Strejcek

Proceedings of the SOFSEM 2005: Theory and Practice of Computer Science, 2005

Reachability of Hennessy-Milner Properties for Weakly Extended PRS.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004

Extended Process Rewrite Systems: Expressiveness and Reachability.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

2003

On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit.

Mojmír Kretínský, Vojtech Rehák, Jan Strejcek

Proceedings of INFINITY 2003, 2003

2002

The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL.

Antonín Kucera, Jan Strejcek

Proceedings of the Computer Science Logic, 16th International Workshop, 2002

2001

Rewrite Systems with Constraints.

Jan Strejcek

Proceedings of the 8th International Workshop on Expressiveness in Concurrency, 2001