Jan Strejcek

According to our database1, Jan Strejcek
  • authored at least 48 papers between 2001 and 2017.
  • has a "Dijkstra number"2 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

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
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F, G)-Fragment.
CoRR, 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.
Mathematical Structures in Computer Science, 2012

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

LTL to Büchi Automata Translation: Fast and More Deterministic
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

2011
Abstracting Path Conditions
CoRR, 2011

2010
Decidable Race Condition and Open Coregions in HMSC.
ECEASST, 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.
Electr. Notes Theor. Comput. Sci., 2009

Almost Linear Büchi Automata
Proceedings of the Proceedings 16th International Workshop on Expressiveness in Concurrency, 2009

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

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

2007
On Symbolic Verification of Weakly Extended PAD.
Electr. Notes Theor. Comput. Sci., 2007

2006
Refining the Undecidability Border of Weak Bisimilarity.
Electr. Notes Theor. Comput. Sci., 2006

On Decidability of LTL Model Checking for Process Rewrite Systems.
Proceedings of the FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 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
The stuttering principle revisited.
Acta Inf., 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

Reachability Analysis of Multithreaded Software with Asynchronous Communication.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit.
Electr. Notes Theor. Comput. Sci., 2004

Extended Process Rewrite Systems: Expressiveness and Reachability.
Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

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


  Loading...