Jan Strejcek - RankMe

98 papers A* 1A 11B 21C 4Journal 25Unranked 35

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