Jan Strejcek

Affiliations:
  • Masaryk University, Brno, Czech Republic


According to our database1, Jan Strejcek authored at least 70 papers between 2001 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage (Technical Report).
CoRR, 2024

2023
Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving.
Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

2022
Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution).
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.
Proceedings of the Static Analysis - 29th International Symposium, 2022

2021
Symbiotic 6: generating test cases by slicing and symbolic execution.
Int. J. Softw. Tools Technol. Transf., 2021

Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

DQBDD: An Efficient BDD-Based DQBF Solver.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2021, 2021

Backward Symbolic Execution with Loop Folding.
Proceedings of the Static Analysis - 28th International Symposium, 2021

Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution).
Proceedings of the Fundamental Approaches to Software Engineering, 2021

Fast Computation of Strong Control Dependencies.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020
LTL to self-loop alternating automata with generic acceptance and back.
Theor. Comput. Sci., 2020

Joint forces for memory safety checking revisited.
Int. J. Softw. Tools Technol. Transf., 2020

Symbiotic 7: Integration of Predator and More - (Competition Contribution).
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.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2020, 2020

Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Evaluation of Program Slicing in Software Verification.
Proceedings of the Integrated Formal Methods - 15th International Conference, 2019

LTL to Smaller Self-Loop Alternating Automata and Back.
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.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2019

Generic Emptiness Check for Fun and Profit.
Proceedings of the Automated Technology for Verification and Analysis, 2019

2018
On the complexity of the quantified bit-vector arithmetic with binary encoding.
Inf. Process. Lett., 2018

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

SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Joint Forces for Memory Safety Checking.
Proceedings of the Model Checking Software - 25th International Symposium, 2018

Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper).
Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2018, 2018

2017
Symbiotic 4: Beyond Reachability - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

On Simplification of Formulas with Unconstrained Variables and Quantifiers.
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.
Proceedings of the LPAR-21, 2017

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

Tighter Loop Bound Analysis (Technical report).
CoRR, 2016

Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Complementing Semi-deterministic Büchi Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

Tighter Loop Bound Analysis.
Proceedings of the Automated Technology for Verification and Analysis, 2016

2015
On Refinement of Büchi Automata for Explicit Model Checking.
Proceedings of the Model Checking Software - 22nd International Symposium, 2015

The Hanoi Omega-Automata Format.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Symbiotic 2: More Precise Slicing - (Competition Contribution).
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?
Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

Symbolic Memory with Pointers.
Proceedings of the Automated Technology for Verification and Analysis, 2014

2013
ClabureDB: Classified Bug-Reports Database.
Proceedings of the Verification, 2013

Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Compositional Approach to Suspension and Other Improvements to LTL Translation.
Proceedings of the Model Checking Software - 20th International Symposium, 2013

Comparison of LTL to Deterministic Rabin Automata Translators.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Compact Symbolic Execution.
Proceedings of the Automated Technology for Verification and Analysis, 2013

Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
Almost linear Büchi automata.
Math. Struct. Comput. Sci., 2012

On Synergy of Metal, Slicing, and Symbolic Execution
CoRR, 2012

LTL to Büchi Automata Translation: Fast and More Deterministic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Abstracting path conditions.
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.
Proceedings of the Formal Methods for Industrial Critical Systems, 2012

2010
Decidable Race Condition and Open Coregions in HMSC.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2010

A Short Story of a Subtle Error in LTL Formulas Reduction and Divine Incorrectness
CoRR, 2010

2009
Reachability is decidable for weakly extended process rewrite systems.
Inf. Comput., 2009

On Decidability of LTL+Past Model Checking for Process Rewrite Systems.
Proceedings of the Joint Proceedings of the 8th, 2009

On decidability of LTL model checking for process rewrite systems.
Acta Informatica, 2009

2008
Petri nets are less expressive than state-extended PA.
Theor. Comput. Sci., 2008

2006
On Symbolic Verification of Weakly Extended PAD.
Proceedings of the 13th International Workshop on Expressiveness in Concurrency, 2006

Reachability analysis of multithreaded software with asynchronous communication.
Proceedings of the Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02., 2006

2005
Refining the Undecidability Border of Weak Bisimilarity.
Proceedings of the 7th International Workshop on Verification of Infinite-State Systems, 2005

The stuttering principle revisited.
Acta Informatica, 2005

Deeper Connections Between LTL and Alternating Automata.
Proceedings of the Implementation and Application of Automata, 2005

Characteristic Patterns for LTL.
Proceedings of the SOFSEM 2005: Theory and Practice of Computer Science, 2005

Reachability of Hennessy-Milner Properties for Weakly Extended PRS.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004
Extended Process Rewrite Systems: Expressiveness and Reachability.
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.
Proceedings of INFINITY 2003, 2003

2002
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL.
Proceedings of the Computer Science Logic, 16th International Workshop, 2002

2001
Rewrite Systems with Constraints.
Proceedings of the 8th International Workshop on Expressiveness in Concurrency, 2001


  Loading...