Computing Simulations over Tree Automata. - Parosh Aziz Abdulla; Ahmed Bouajjani; Lukás Holík; Lisa Kaati; Tomás Vojnar (TACAS, 2008)

Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. - Ahmed Bouajjani; Peter Habermehl; Lukás Holík; Tayssir Touili; Tomás Vojnar (CIAA, 2008)

A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. - Parosh Aziz Abdulla; Lukás Holík; Lisa Kaati; Tomás Vojnar (MEMICS, 2008)

Composed Bisimulation for Tree Automata. - Parosh Aziz Abdulla; Ahmed Bouajjani; Lukás Holík; Lisa Kaati; Tomás Vojnar (Int. J. Found. Comput. Sci., 2009)

Simulation Subsumption in Ramsey-Based Büchi Automata Universality and Inclusion Testing. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lorenzo Clemente; Lukás Holík; Chih-Duo Hong; Richard Mayr; Tomás Vojnar (CAV, 2010)

When Simulation Meets Antichains. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lukás Holík; Richard Mayr; Tomás Vojnar (TACAS, 2010)

Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata. - Lukás Holík; Ondrej Lengál; Jirí Simácek; Tomás Vojnar (ATVA, 2011)

Advanced Ramsey-Based Büchi Automata Inclusion Testing. - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lorenzo Clemente; Lukás Holík; Chih-Duo Hong; Richard Mayr; Tomás Vojnar (CONCUR, 2011)

Forest automata for verification of heap manipulation. - Peter Habermehl; Lukás Holík; Adam Rogalewicz; Jirí Simácek; Tomás Vojnar (Formal Methods Syst. Des., 2012)

Fully Automated Shape Analysis Based on Forest Automata. - Lukás Holík; Ondrej Lengál; Adam Rogalewicz; Jirí Simácek; Tomás Vojnar (CAV, 2013)

All for the Price of Few. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík (VMCAI, 2013)

String Constraints for Verification. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV, 2014)

Block Me If You Can! - Context-Sensitive Parameterized Verification. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík (SAS, 2014)

Mediating for reduction (on minimizing alternating Büchi automata). - Parosh Aziz Abdulla; Yu-Fang Chen 001; Lukás Holík; Tomás Vojnar (Theor. Comput. Sci., 2014)

Mediator Synthesis in a Component Algebra with Data. - Lukás Holík; Malte Isberner; Bengt Jonsson 001 (Correct System Design, 2015)

Norn: An SMT Solver for String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV (1), 2015)

Antichains for the Verification of Recursive Programs. - Lukás Holík; Roland Meyer 001 (NETYS, 2015)

View Abstraction - A Tutorial (Invited Paper). - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík (SynCoP, 2015)

Forester: Shape Analysis Using Tree Automata - (Competition Contribution). - Lukás Holík; Martin Hruska; Ondrej Lengál; Adam Rogalewicz; Jirí Simácek; Tomás Vojnar (TACAS, 2015)

Summaries for Context-Free Games. - Lukás Holík; Roland Meyer 001; Sebastian Muskalla (FSTTCS, 2016)

Predator Shape Analysis Tool Suite. - Lukás Holík; Michal Kotoun; Petr Peringer; Veronika Soková; Marek Trtík; Tomás Vojnar (Haifa Verification Conference, 2016)

Reduction of Nondeterministic Tree Automata. - Ricardo Almeida 003; Lukás Holík; Richard Mayr (TACAS, 2016)

Run Forester, Run Backwards! - (Competition Contribution). - Lukás Holík; Martin Hruska; Ondrej Lengál; Adam Rogalewicz; Jirí Simácek; Tomás Vojnar (TACAS, 2016)

From Low-Level Pointers to High-Level Containers. - Kamil Dudka; Lukás Holík; Petr Peringer; Marek Trtík; Tomás Vojnar (VMCAI, 2016)

Pointer Race Freedom. - Frédéric Haziza; Lukás Holík; Roland Meyer 001; Sebastian Wolff 001 (VMCAI, 2016)

Verification of heap manipulating programs with ordered data by extended forest automata. - Parosh Aziz Abdulla; Lukás Holík; Bengt Jonsson 001; Ondrej Lengál; Cong Quy Trinh; Tomás Vojnar (Acta Informatica, 2016)

Antichains for Inclusion Games. - Lukás Holík; Roland Meyer 001; Sebastian Muskalla (CoRR, 2016)

Parameterized verification through view abstraction. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík (Int. J. Softw. Tools Technol. Transf., 2016)

Towards Smaller Invariants for Proving Coverability. - Lenka Turonová; Lukás Holík (EUROCAST (2), 2017)

Flatten and conquer: a framework for efficient analysis of string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (PLDI, 2017)

Effect Summaries for Thread-Modular Analysis - Sound Analysis Despite an Unsound Heuristic. - Lukás Holík; Roland Meyer 001; Tomás Vojnar; Sebastian Wolff 001 (SAS, 2017)

Lazy Automata Techniques for WS1S. - Tomás Fiedor; Lukás Holík; Petr Janku; Ondrej Lengál; Tomás Vojnar (TACAS (1), 2017)

Forester: From Heap Shapes to Automata Predicates - (Competition Contribution). - Lukás Holík; Martin Hruska; Ondrej Lengál; Adam Rogalewicz; Jirí Simácek; Tomás Vojnar (TACAS (2), 2017)

Counterexample Validation and Interpolation-Based Refinement for Forest Automata. - Lukás Holík; Martin Hruska; Ondrej Lengál; Adam Rogalewicz; Tomás Vojnar (VMCAI, 2017)

Simulations and Antichains for Efficient Handling of Finite Automata. - Lukás Holík (CoRR, 2017)

Effect Summaries for Thread-Modular Analysis. - Lukás Holík; Roland Meyer 001; Tomás Vojnar; Sebastian Wolff 001 (CoRR, 2017)

An integrated specification and verification technique for highly concurrent data structures. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík; Bengt Jonsson 001; Ahmed Rezine (Int. J. Softw. Tools Technol. Transf., 2017)

Simulation Algorithms for Symbolic Automata. - Lukás Holík; Ondrej Lengál; Juraj Síc; Margus Veanes; Tomás Vojnar (ATVA, 2018)

Trau: SMT solver for string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (FMCAD, 2018)

From Shapes to Amortized Complexity. - Tomás Fiedor; Lukás Holík; Adam Rogalewicz; Moritz Sinn; Tomás Vojnar; Florian Zuleger (VMCAI, 2018)

Simulation Algorithms for Symbolic Automata (Technical Report). - Lukás Holík; Ondrej Lengál; Juraj Síc; Margus Veanes; Tomás Vojnar (CoRR, 2018)

String constraints with concatenation and transducers solved efficiently. - Lukás Holík; Petr Janku; Anthony W. Lin; Philipp Rümmer; Tomás Vojnar (Proc. ACM Program. Lang., 2018)

J-ReCoVer: Java Reducer Commutativity Verifier. - Yu-Fang Chen 001; Chang-Yi Chiang; Lukás Holík; Wei-Tsung Kao; Hsin-Hung Lin; Tomás Vojnar; Yean-Fu Wen; Wei-Cheng Wu (APLAS, 2019)

Succinct Determinisation of Counting Automata via Sphere Construction. - Lukás Holík; Ondrej Lengál; Olli Saarikivi; Lenka Turonová; Margus Veanes; Tomás Vojnar (APLAS, 2019)

Chain-Free String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bui Phi Diep; Lukás Holík; Petr Janku (ATVA, 2019)

Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. - Milan Ceska 002; Vojtech Havlena; Lukás Holík; Jan Korenek; Ondrej Lengál; Denis Matousek; Jirí Matousek 002; Jakub Semric; Tomás Vojnar (FCCM, 2019)

Nested antichains for WS1S. - Tomás Fiedor; Lukás Holík; Ondrej Lengál; Tomás Vojnar (Acta Informatica, 2019)

Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. - Milan Ceska 001; Vojtech Havlena; Lukás Holík; Jan Korenek; Ondrej Lengál; Denis Matousek; Jirí Matousek 002; Jakub Semric; Tomás Vojnar (CoRR, 2019)

Automata Terms in a Lazy WSkS Decision Procedure (Technical Report). - Vojtech Havlena; Lukás Holík; Ondrej Lengál; Tomás Vojnar (CoRR, 2019)

Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report). - Lukás Holík; Ondrej Lengál; Olli Saarikivi; Lenka Turonová; Margus Veanes; Tomás Vojnar (CoRR, 2019)

Forester Virtual Machine. - Ondrej Lengál; Lukás Holík; Tomás Vojnar; Adam Rogalewicz; Jirí Simácek; Martin Hruska; Peter Habermehl (Zenodo, 2019)

Antiprenexing for WSkS: A Little Goes a Long Way. - Vojtech Havlena; Lukás Holík; Ondrej Lengál; Ondrej Vales; Tomás Vojnar (LPAR, 2020)

Efficient handling of string-number conversion. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Julian Dolby; Petr Janku; Hsin-Hung Lin; Lukás Holík; Wei-Cheng Wu (PLDI, 2020)

String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report). - Lukás Holík; Petr Janku; Anthony W. Lin; Philipp Rümmer; Tomás Vojnar (CoRR, 2020)

Abstraction refinement and antichains for trace inclusion of infinite state systems. - Lukás Holík; Radu Iosif; Adam Rogalewicz; Tomás Vojnar (Formal Methods Syst. Des., 2020)

Regex matching with counting-set automata. - Lenka Turonová; Lukás Holík; Ondrej Lengál; Olli Saarikivi; Margus Veanes; Tomás Vojnar (Proc. ACM Program. Lang., 2020)

Approximate reduction of finite automata for high-speed network intrusion detection. - Milan Ceska 002; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Tomás Vojnar (Int. J. Softw. Tools Technol. Transf., 2020)

Dataset for the OOPSLA'20 paper "Regex Matching with Counting-Set Automata". - Lukás Holík; Ondrej Lengál; Olli Saarikivi; Lenka Turonová; Margus Veanes; Tomás Vojnar (Zenodo, 2020)

Dataset for the OOPSLA'20 paper "Regex Matching with Counting-Set Automata". - Lukás Holík; Ondrej Lengál; Olli Saarikivi; Lenka Turonová; Margus Veanes; Tomás Vojnar (Zenodo, 2020)

Artifact for the OOPSLA'20 paper "Regex Matching with Counting-Set Automata". - Lukás Holík; Ondrej Lengál; Olli Saarikivi; Lenka Turonová; Margus Veanes; Tomás Vojnar (Zenodo, 2020)

Solving Not-Substring Constraint withFlat Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Denghang Hu; Wei-Lun Tsai; Zhilin Wu; Di-De Yen (APLAS, 2021)

Simplifying Alternating Automata for Emptiness Testing. - Pavol Vargovcík; Lukás Holík (APLAS, 2021)

Efficient Modelling of ICS Communication For Anomaly Detection Using Probabilistic Automata. - Petr Matousek; Vojtech Havlena; Lukás Holík (IM, 2021)

Towards Efficient Shape Analysis with Tree Automata. - Martin Hruska; Lukás Holík (NETYS, 2021)

Automata Terms in a Lazy WSkS Decision Procedure. - Vojtech Havlena; Lukás Holík; Ondrej Lengál; Tomás Vojnar (J. Autom. Reason., 2021)

Correction to: An integrated specification and verification technique for highly concurrent data structures. - Parosh Aziz Abdulla; Frédéric Haziza; Lukás Holík; Bengt Jonsson 001; Ahmed Rezine (Int. J. Softw. Tools Technol. Transf., 2021)

Low-Level Bi-Abduction. - Lukás Holík; Petr Peringer; Adam Rogalewicz; Veronika Soková; Tomás Vojnar; Florian Zuleger (ECOOP, 2022)

Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. - Lenka Turonová; Lukás Holík; Ivan Homoliak; Ondrej Lengál; Margus Veanes; Tomás Vojnar (USENIX Security Symposium, 2022)

Word Equations in Synergy with Regular Constraints (Technical Report). - Frantisek Blahoudek; Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (CoRR, 2022)

Low-Level Bi-Abduction (Artifact). - Lukás Holík; Petr Peringer; Adam Rogalewicz; Veronika Soková; Tomás Vojnar; Florian Zuleger (Dagstuhl Artifacts Ser., 2022)

Reasoning About Regular Properties: A Comparative Study. - Tomás Fiedor; Lukás Holík; Martin Hruska; Adam Rogalewicz; Juraj Síc; Pavol Vargovcík (CADE, 2023)

Word Equations in Synergy with Regular Constraints. - Frantisek Blahoudek; Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (FM, 2023)

Fast Matching of Regular Patterns with Synchronizing Counting. - Lukás Holík; Juraj Síc; Lenka Turonová; Tomás Vojnar (FoSSaCS, 2023)

Fast Matching of Regular Patterns with Synchronizing Counting (Technical Report). - Lukás Holík; Juraj Síc; Lenka Turonová; Tomás Vojnar (CoRR, 2023)

Chain-Free String Constraints (Technical Report). - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bui Phi Diep; Lukás Holík; Petr Janku (CoRR, 2023)

Optimizing an LTS-Simulation Algorithm (Technical Report). - Lukás Holík; Jirí Simácek (CoRR, 2023)

Z3-Noodler: An Automata-based String Solver (Technical Report). - Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (CoRR, 2023)

Mata, a Fast and Simple Finite Automata Library (Technical Report). - David Chocholatý; Tomás Fiedor; Vojtech Havlena; Lukás Holík; Martin Hruska; Ondrej Lengál; Juraj Síc (CoRR, 2023)

Accurate Automata-Based Detection of Cyber Threats in Smart Grid Communication. - Vojtech Havlena; Petr Matousek; Ondrej Rysavý; Lukás Holík (IEEE Trans. Smart Grid, 2023)

Solving String Constraints with Lengths by Stabilization. - Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (Proc. ACM Program. Lang., 2023)

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. - Peter Habermehl; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CAV (1), 2024)

Cooking String-Integer Conversions with Noodles. - Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (SAT, 2024)

Antichain with SAT and Tries. - Lukás Holík; Pavol Vargovcík (SAT, 2024)

Z3-Noodler: An Automata-based String Solver. - Yu-Fang Chen 001; David Chocholatý; Vojtech Havlena; Lukás Holík; Ondrej Lengál; Juraj Síc (TACAS (1), 2024)

Mata: A Fast and Simple Finite Automata Library. - David Chocholatý; Tomás Fiedor; Vojtech Havlena; Lukás Holík; Martin Hruska; Ondrej Lengál; Juraj Síc (TACAS (2), 2024)

Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report). - Parosh Aziz Abdulla; Yo-Ga Chen; Yu-Fang Chen 001; Lukás Holík; Ondrej Lengál; Jyun-Ao Lin; Fang-Yi Lo; Wei-Lun Tsai (CoRR, 2024)

Negated String Containment Is Decidable. - Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (MFCS, 2025)

Automata Size Reduction by Procedure Finding. - Michal Sedý; Lukás Holík (NFM, 2025)

Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. - David Chocholatý; Vojtech Havlena; Lukás Holík; Jan Hranicka; Ondrej Lengál; Juraj Síc (TACAS (2), 2025)

Verifying Quantum Circuits with Level-Synchronized Tree Automata. - Parosh Aziz Abdulla; Yo-Ga Chen; Yu-Fang Chen 001; Lukás Holík; Ondrej Lengál; Jyun-Ao Lin; Fang-Yi Lo; Wei-Lun Tsai (Proc. ACM Program. Lang., 2025)

A Uniform Framework for Handling Position Constraints in String Solving. - Yu-Fang Chen 001; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (Proc. ACM Program. Lang., 2025)

A Uniform Framework for Handling Position Constraints in String Solving (Technical Report). - Yu-Fang Chen 001; Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CoRR, 2025)

Negated String Containment is Decidable (Technical Report). - Vojtech Havlena; Michal Hecko; Lukás Holík; Ondrej Lengál (CoRR, 2025)

On Complementation of Nondeterministic Finite Automata without Full Determinization (Technical Report). - Lukás Holík; Ondrej Lengál; Juraj Major; Adéla Stepková; Jan Strejcek (CoRR, 2025)