default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJan Strejcek
Person information
- affiliation: Masaryk University, Brno, Czech Republic
- unicode name: Jan Strejček
SPARQL queries 
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j11]Martin Jonás, Jan Strejcek:
Truncating abstraction of bit-vector operations for BDD-based SMT solvers. Theor. Comput. Sci. 1008: 114664 (2024)- [c62]Martin Jonás
, Jan Strejcek, Marek Trtík, Lukás Urban:
Fizzer: New Gray-Box Fuzzer - (Competition Contribution). FASE 2024: 309-313 - [c61]Marek Jankola, Jan Strejcek:
Tighter Construction of Tight Büchi Automata. FoSSaCS (1) 2024: 234-255 - [c60]Paulína Ayaziová, Dirk Beyer, Marian Lingsch Rosenfeld, Martin Spiessl, Jan Strejcek:
Software Verification Witnesses 2.0. SPIN 2024: 184-203 - [c59]Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban:
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage. TACAS (3) 2024: 90-109 - [c58]Paulína Ayaziová, Jan Strejcek:
Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution). TACAS (3) 2024: 341-346 - [c57]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: 406-411 - [i12]Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban:
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage (Technical Report). CoRR abs/2401.12643 (2024) - 2023
- [c56]Tereza Schwarzová, Jan Strejcek, Juraj Major:
Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. SAT 2023: 23:1-23:20 - [c55]Paulína Ayaziová, Jan Strejcek:
Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution). TACAS (2) 2023: 523-528 - [d2]Paulína Ayaziová, Dirk Beyer, Marian Lingsch Rosenfeld, Martin Spiessl, Jan Strejcek:
Reproduction Package for FSE 2024 Submission 'Verification Witnesses Version 2'. Zenodo, 2023
- 2022
- [c54]Dirk Beyer, Jan Strejcek:
Case Study on Verification-Witness Validators: Where We Are and Where We Go. SAS 2022: 160-174 - [c53]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: 462-467 - [c52]Paulína Ayaziová, Marek Chalupa, Jan Strejcek:
Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution). TACAS (2) 2022: 468-473 - [d1]Dirk Beyer, Jan Strejcek:
Reproduction Package for SAS 2022 Article 'Case Study on Verification-Witness Validators: Where We Are and Where We Go'. Zenodo, 2022 - 2021
- [j10]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): 875-877 (2021) - [c51]Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic:
Fast Computation of Strong Control Dependencies. CAV (2) 2021: 887-910 - [c50]Marek Chalupa, Jakub Novák, Jan Strejcek:
Symbiotic 8: Parallel and Targeted Test Generation - (Competition Contribution). FASE 2021: 368-372 - [c49]Marek Chalupa, Jan Strejcek:
Backward Symbolic Execution with Loop Folding. SAS 2021: 49-76 - [c48]Juraj Síc, Jan Strejcek:
DQBDD: An Efficient BDD-Based DQBF Solver. SAT 2021: 535-544 - [c47]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: 453-457 - 2020
- [j9]Marek Chalupa, Jan Strejcek, Martina Vitovská:
Joint forces for memory safety checking revisited. Int. J. Softw. Tools Technol. Transf. 22(2): 115-133 (2020) - [j8]Frantisek Blahoudek, Juraj Major, Jan Strejcek:
LTL to self-loop alternating automata with generic acceptance and back. Theor. Comput. Sci. 840: 122-142 (2020) - [c46]Frantisek Blahoudek, Alexandre Duret-Lutz, Jan Strejcek:
Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization. CAV (2) 2020: 15-27 - [c45]Martin Jonás, Jan Strejcek:
Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. SAT 2020: 378-393 - [c44]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: 413-417 - [i11]Marek Chalupa, David Klaska, Jan Strejcek, Lukás Tomovic:
Fast Computation of Strong Control Dependencies. CoRR abs/2011.01564 (2020)
2010 – 2019
- 2019
- [c43]Juraj Major, Frantisek Blahoudek, Jan Strejcek, Miriama Sasaráková, Tatiana Zboncáková:
ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. ATVA 2019: 357-365 - [c42]Christel Baier, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, Jan Strejcek:
Generic Emptiness Check for Fun and Profit. ATVA 2019: 445-461 - [c41]Martin Jonás, Jan Strejcek:
Q3B: An Efficient BDD-based SMT Solver for Quantified Bit-Vectors. CAV (2) 2019: 64-73 - [c40]Frantisek Blahoudek, Juraj Major, Jan Strejcek:
LTL to Smaller Self-Loop Alternating Automata and Back. ICTAC 2019: 152-171 - [c39]Marek Chalupa, Jan Strejcek:
Evaluation of Program Slicing in Software Verification. IFM 2019: 101-119 - [i10]Frantisek Blahoudek, Juraj Major, Jan Strejcek:
LTL to Smaller Self-Loop Alternating Automata and Back. CoRR abs/1908.04645 (2019) - 2018
- [j7]Martin Jonás, Jan Strejcek:
On the complexity of the quantified bit-vector arithmetic with binary encoding. Inf. Process. Lett. 135: 57-61 (2018) - [c38]Martin Jonás, Jan Strejcek:
Abstraction of Bit-Vector Operations for BDD-Based SMT Solvers. ICTAC 2018: 273-291 - [c37]Martin Jonás, Jan Strejcek:
Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Experimental Paper). LPAR 2018: 488-497 - [c36]Marek Chalupa, Jan Strejcek, Martina Vitovská:
Joint Forces for Memory Safety Checking. SPIN 2018: 115-132 - [c35]Marek Chalupa, Martina Vitovská, Jan Strejcek:
SYMBIOTIC 5: Boosted Instrumentation - (Competition Contribution). TACAS (2) 2018: 442-446 - [i9]Martina Vitovská, Marek Chalupa, Jan Strejcek:
SBT-instrumentation: A Tool for Configurable Instrumentation of LLVM Bitcode. CoRR abs/1810.12617 (2018) - 2017
- [c34]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: 356-367 - [c33]Martin Jonás, Jan Strejcek:
On Simplification of Formulas with Unconstrained Variables and Quantifiers. SAT 2017: 364-379 - [c32]Marek Chalupa, Martina Vitovská, Martin Jonás, Jiri Slaby, Jan Strejcek:
Symbiotic 4: Beyond Reachability - (Competition Contribution). TACAS (2) 2017: 385-389 - 2016
- [c31]Pavel Cadek, Jan Strejcek, Marek Trtík:
Tighter Loop Bound Analysis. ATVA 2016: 512-527 - [c30]Martin Jonás, Jan Strejcek:
Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. SAT 2016: 267-283 - [c29]Frantisek Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejcek, Ming-Hsien Tsai:
Complementing Semi-deterministic Büchi Automata. TACAS 2016: 770-787 - [c28]Marek Chalupa, Martin Jonás, Jiri Slaby, Jan Strejcek, Martina Vitovská:
Symbiotic 3: New Slicer and Error-Witness Generation - (Competition Contribution). TACAS 2016: 946-949 - [e1]Jan Bouda, Lukás Holík, Jan Kofron, Jan Strejcek, Adam Rambousek:
Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS 2016, Telč, Czech Republic, 21st-23rd October 2016. EPTCS 233, 2016 [contents] - [i8]Pavel Cadek, Jan Strejcek, Marek Trtík:
Tighter Loop Bound Analysis (Technical report). CoRR abs/1605.03636 (2016) - [i7]Martin Jonás, Jan Strejcek:
On the Complexity of the Quantified Bit-Vector Arithmetic with Binary Encoded Bit-Widths. CoRR abs/1612.01263 (2016) - 2015
- [c27]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: 479-486 - [c26]Frantisek Blahoudek, Alexandre Duret-Lutz, Vojtech Rujbr, Jan Strejcek:
On Refinement of Büchi Automata for Explicit Model Checking. SPIN 2015: 66-83 - 2014
- [c25]Marek Trtík, Jan Strejcek:
Symbolic Memory with Pointers. ATVA 2014: 380-395 - [c24]Frantisek Blahoudek, Alexandre Duret-Lutz, Mojmír Kretínský, Jan Strejcek:
Is there a best büchi automaton for explicit model checking? SPIN 2014: 68-76 - [c23]Jiri Slaby, Jan Strejcek:
Symbiotic 2: More Precise Slicing - (Competition Contribution). TACAS 2014: 415-417 - 2013
- [c22]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: 24-39 - [c21]Jiri Slaby, Jan Strejcek, Marek Trtík:
Compact Symbolic Execution. ATVA 2013: 193-207 - [c20]Frantisek Blahoudek, Mojmír Kretínský, Jan Strejcek:
Comparison of LTL to Deterministic Rabin Automata Translators. LPAR 2013: 164-172 - [c19]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: 81-98 - [c18]Jiri Slaby, Jan Strejcek, Marek Trtík:
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution - (Competition Contribution). TACAS 2013: 630-632 - [c17]Jiri Slaby, Jan Strejcek, Marek Trtík:
ClabureDB: Classified Bug-Reports Database. VMCAI 2013: 268-274 - [i6]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 abs/1306.4636 (2013) - 2012
- [j6]Tomás Babiak, Vojtech Rehák, Jan Strejcek:
Almost linear Büchi automata. Math. Struct. Comput. Sci. 22(2): 203-235 (2012) - [c16]Jiri Slaby, Jan Strejcek, Marek Trtík:
Checking Properties Described by State Machines: On Synergy of Instrumentation, Slicing, and Symbolic Execution. FMICS 2012: 207-221 - [c15]Jan Strejcek, Marek Trtík:
Abstracting path conditions. ISSTA 2012: 155-165 - [c14]Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
LTL to Büchi Automata Translation: Fast and More Deterministic. TACAS 2012: 95-109 - [i5]Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
LTL to Büchi Automata Translation: Fast and More Deterministic. CoRR abs/1201.0682 (2012) - [i4]Jiri Slaby, Jan Strejcek, Marek Trtík:
On Synergy of Metal, Slicing, and Symbolic Execution. CoRR abs/1201.4719 (2012) - 2011
- [i3]Jan Strejcek, Marek Trtík:
Abstracting Path Conditions. CoRR abs/1112.5671 (2011) - 2010
- [j5]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) - [i2]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 abs/1011.4214 (2010)
2000 – 2009
- 2009
- [j4]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): 1-28 (2009) - [j3]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
Reachability is decidable for weakly extended process rewrite systems. Inf. Comput. 207(6): 671-680 (2009) - [c13]Tomás Babiak, Vojtech Rehák, Jan Strejcek:
Almost Linear Büchi Automata. EXPRESS 2009: 16-25 - [c12]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
On Decidability of LTL+Past Model Checking for Process Rewrite Systems. INFINITY 2009: 105-117 - 2008
- [j2]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
Petri nets are less expressive than state-extended PA. Theor. Comput. Sci. 394(1-2): 134-140 (2008) - 2006
- [c11]Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
On Decidability of LTL Model Checking for Process Rewrite Systems. FSTTCS 2006: 248-259 - [c10]Ahmed Bouajjani, Jan Strejcek, Tayssir Touili:
On Symbolic Verification of Weakly Extended PAD. EXPRESS 2006: 47-64 - [i1]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 - 2005
- [j1]Antonín Kucera, Jan Strejcek:
The stuttering principle revisited. Acta Informatica 41(7-8): 415-434 (2005) - [c9]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
Reachability of Hennessy-Milner Properties for Weakly Extended PRS. FSTTCS 2005: 213-224 - [c8]Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek:
Reachability Analysis of Multithreaded Software with Asynchronous Communication. FSTTCS 2005: 348-359 - [c7]Antonín Kucera, Jan Strejcek:
Characteristic Patterns for LTL. SOFSEM 2005: 239-249 - [c6]Radek Pelánek, Jan Strejcek:
Deeper Connections Between LTL and Alternating Automata. CIAA 2005: 238-249 - [c5]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
Refining the Undecidability Border of Weak Bisimilarity. INFINITY 2005: 17-36 - 2004
- [c4]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
Extended Process Rewrite Systems: Expressiveness and Reachability. CONCUR 2004: 355-370 - 2003
- [c3]Mojmír Kretínský, Vojtech Rehák, Jan Strejcek:
On Extensions of Process Rewrite Systems: Rewrite Systems with Weak Finite-State Unit. INFINITY 2003: 75-88 - 2002
- [c2]Antonín Kucera, Jan Strejcek:
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL. CSL 2002: 276-291 - 2001
- [c1]Jan Strejcek:
Rewrite Systems with Constraints. EXPRESS 2001: 46-65
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 20:48 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
