Ondrej Lengál

98 papers A* 5A 7B 15C 2Misc 1Journal 46Unranked 21
YearRankTypeTitle / Venue / Authors
2026 J jnl
Parameterized Verification of Quantum Circuits.
Proc. ACM Program. Lang.
Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hecko, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Ramanathan S. Thinniyam
2026 B ed.
Verification, Model Checking, and Abstract Interpretation - 27th International Conference, VMCAI 2026, Rennes, France, January 12-13, 2026, Proceedings
VMCAI
Yu-Fang Chen, Thomas P. Jensen, Ondrej Lengál
2025 J jnl
A Uniform Framework for Handling Position Constraints in String Solving (Technical Report).
CoRR
Yu-Fang Chen, Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál
2025 J jnl
A Uniform Framework for Handling Position Constraints in String Solving.
Proc. ACM Program. Lang.
Yu-Fang Chen, Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál
2025 J jnl
An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.
Commun. ACM
Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
2025 — conf
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs.
TACAS (3)
Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai
2025 B conf
Complementation of Emerson-Lei Automata.
FoSSaCS
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2025 B conf
Negated String Containment Is Decidable.
MFCS
Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál
2025 J jnl
Negated String Containment is Decidable (Technical Report).
CoRR
Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál
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
2025 — conf
On the Verification of Quantum Circuits (Research Challenges and Opportunities).
Principles of Formal Quantitative Analysis
Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Kai-Min Chung, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai
2025 J jnl
Parameterized Verification of Quantum Circuits (Technical Report).
CoRR
Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hecko, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Ramanathan S. Thinniyam
2025 — conf
Quantum Circuit Verification - A Potential Roadmap (Invited Talk).
FSTTCS
Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hecko, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Ramanathan Thinniyam Srinivasan
2025 J jnl
Verifying Quantum Circuits with Level-Synchronized Tree Automata.
Proc. ACM Program. Lang.
Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai
2025 J jnl
Word equations in synergy with regular constraints (extended version).
Constraints An Int. J.
Frantisek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2025 — conf
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation.
TACAS (2)
David Chocholatý, Vojtech Havlena, Lukás Holík, Jan Hranicka, Ondrej Lengál, Juraj Síc
2024 A conf
Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization.
ICCAD
Tian-Fu Chen, Yu-Fang Chen, Jie-Hong Roland Jiang, Sára Jobranová, Ondrej Lengál
2024 — conf
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic.
CAV (1)
Peter Habermehl, Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál
2024 J jnl
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic.
CoRR
Peter Habermehl, Michal Hecko, Vojtech Havlena, Lukás Holík, Ondrej Lengál
2024 J jnl
AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs.
CoRR
Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai
2024 J jnl
Complementation of Emerson-Lei Automata (Technical Report).
CoRR
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2024 A conf
Cooking String-Integer Conversions with Noodles.
SAT
Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2024 — conf
Mata: A Fast and Simple Finite Automata Library.
TACAS (2)
David Chocholatý, Tomás Fiedor, Vojtech Havlena, Lukás Holík, Martin Hruska, Ondrej Lengál, Juraj Síc
2024 J jnl
Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report).
CoRR
Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukás Holík, Ondrej Lengál, Jyun-Ao Lin, Fang-Yi Lo, Wei-Lun Tsai
2024 — conf
Z3-Noodler: An Automata-based String Solver.
TACAS (1)
Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2023 J jnl
A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report).
CoRR
Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál, Andrea Turrini
2023 J jnl
A symbolic algorithm for the case-split rule in solving word constraints with extensions.
J. Syst. Softw.
Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál, Andrea Turrini
2023 J jnl
An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.
Proc. ACM Program. Lang.
Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
2023 J jnl
An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report).
CoRR
Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
2023 — conf
AutoQ: An Automata-Based Quantum Circuit Verifier.
CAV (3)
Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai
2023 J jnl
Mata, a Fast and Simple Finite Automata Library (Technical Report).
CoRR
David Chocholatý, Tomás Fiedor, Vojtech Havlena, Lukás Holík, Martin Hruska, Ondrej Lengál, Juraj Síc
2023 J jnl
Modular Mix-and-Match Complementation of Büchi Automata (Technical Report).
CoRR
Vojtech Havlena, Ondrej Lengál, Yong Li, Barbora Smahlíková, Andrea Turrini
2023 — conf
Modular Mix-and-Match Complementation of Büchi Automata.
TACAS (1)
Vojtech Havlena, Ondrej Lengál, Yong Li, Barbora Smahlíková, Andrea Turrini
2023 J jnl
Solving String Constraints with Lengths by Stabilization.
Proc. ACM Program. Lang.
Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2023 B conf
Word Equations in Synergy with Regular Constraints.
FM
Frantisek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2023 J jnl
Z3-Noodler: An Automata-based String Solver (Technical Report).
CoRR
Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2022 J jnl
Complementing Büchi Automata with Ranker (Technical Report).
CoRR
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2022 — conf
Complementing Büchi Automata with Ranker.
CAV (2)
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2022 A* conf
Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers.
USENIX Security Symposium
Lenka Turonová, Lukás Holík, Ivan Homoliak, Ondrej Lengál, Margus Veanes, Tomás Vojnar
2022 J jnl
Register Set Automata (Technical Report).
CoRR
Sabína Gulcíková, Ondrej Lengál
2022 — conf
Sky Is Not the Limit - Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation.
TACAS (2)
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2022 J jnl
Word Equations in Synergy with Regular Constraints (Technical Report).
CoRR
Frantisek Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
2021 J jnl
Automata Terms in a Lazy WSkS Decision Procedure.
J. Autom. Reason.
Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2021 — conf
Deciding S1S: Down the Rabbit Hole and Through the Looking Glass.
NETYS
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2021 B conf
Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation.
CONCUR
Vojtech Havlena, Ondrej Lengál
2021 J jnl
Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation (Technical Report).
CoRR
Vojtech Havlena, Ondrej Lengál, Barbora Smahlíková
2020 B conf
A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving.
APLAS
Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál, Andrea Turrini
2020 B conf
Antiprenexing for WSkS: A Little Goes a Long Way.
LPAR
Vojtech Havlena, Lukás Holík, Ondrej Lengál, Ondrej Vales, Tomás Vojnar
2020 J jnl
Approximate reduction of finite automata for high-speed network intrusion detection.
Int. J. Softw. Tools Technol. Transf.
Milan Ceska, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2020 J jnl
Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report).
CoRR
Vojtech Havlena, Ondrej Lengál
2020 J jnl
Regex matching with counting-set automata.
Proc. ACM Program. Lang.
Lenka Turonová, Lukás Holík, Ondrej Lengál, Olli Saarikivi, Margus Veanes, Tomás Vojnar
2019 J jnl
Automata Terms in a Lazy WSkS Decision Procedure (Technical Report).
CoRR
Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2019 A conf
Automata Terms in a Lazy WSkS Decision Procedure.
CADE
Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2019 Misc conf
Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata.
FCCM
Milan Ceska, Vojtech Havlena, Lukás Holík, Jan Korenek, Ondrej Lengál, Denis Matousek, Jirí Matousek, Jakub Semric, Tomás Vojnar
2019 J jnl
Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata.
CoRR
Milan Ceska, Vojtech Havlena, Lukás Holík, Jan Korenek, Ondrej Lengál, Denis Matousek, Jirí Matousek, Jakub Semric, Tomás Vojnar
2019 J jnl
Nested antichains for WS1S.
Acta Informatica
Tomás Fiedor, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2019 — conf
SL-COMP: Competition of Solvers for Separation Logic.
TACAS (3)
Mihaela Sighireanu, Juan Antonio Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomás Vojnar, Constantin Enea, Ondrej Lengál, Chong Gao, Zhilin Wu
2019 B conf
Simulations in Rank-Based Büchi Automata Complementation.
APLAS
Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál
2019 J jnl
Simulations in Rank-Based Büchi Automata Complementation.
CoRR
Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál
2019 J jnl
Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report).
CoRR
Lukás Holík, Ondrej Lengál, Olli Saarikivi, Lenka Turonová, Margus Veanes, Tomás Vojnar
2019 B conf
Succinct Determinisation of Counting Automata via Sphere Construction.
APLAS
Lukás Holík, Ondrej Lengál, Olli Saarikivi, Lenka Turonová, Margus Veanes, Tomás Vojnar
2018 A* conf
Advanced automata-based algorithms for program termination checking.
PLDI
Yu-Fang Chen, Matthias Heizmann, Ondrej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, Lijun Zhang
2018 — conf
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection.
TACAS (2)
Milan Ceska, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2018 J jnl
Simulation Algorithms for Symbolic Automata (Technical Report).
CoRR
Lukás Holík, Ondrej Lengál, Juraj Síc, Margus Veanes, Tomás Vojnar
2018 B conf
Simulation Algorithms for Symbolic Automata.
ATVA
Lukás Holík, Ondrej Lengál, Juraj Síc, Margus Veanes, Tomás Vojnar
2017 — conf
An Executable Sequential Specification for Spark Aggregation.
NETYS
Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengál, Shin-Cheng Mu, Nishant Sinha, Bow-Yaw Wang
2017 J jnl
An Executable Sequential Specification for Spark Aggregation.
CoRR
Yu-Fang Chen, Chih-Duo Hong, Ondrej Lengál, Shin-Cheng Mu, Nishant Sinha, Bow-Yaw Wang
2017 J jnl
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection.
CoRR
Milan Ceska, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2017 J jnl
Compositional entailment checking for a fragment of separation logic.
Formal Methods Syst. Des.
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, Tomás Vojnar
2017 B conf
Counterexample Validation and Interpolation-Based Refinement for Forest Automata.
VMCAI
Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Tomás Vojnar
2017 J jnl
Fair Termination for Parameterized Probabilistic Concurrent Systems (Technical Report).
CoRR
Ondrej Lengál, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer
2017 — conf
Fair Termination for Parameterized Probabilistic Concurrent Systems.
TACAS (1)
Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, Philipp Rümmer
2017 — conf
Forester: From Heap Shapes to Automata Predicates - (Competition Contribution).
TACAS (2)
Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
2017 — conf
Lazy Automata Techniques for WS1S.
TACAS (1)
Tomás Fiedor, Lukás Holík, Petr Janku, Ondrej Lengál, Tomás Vojnar
2017 J jnl
Lazy Automata Techniques for WS1S.
CoRR
Tomás Fiedor, Lukás Holík, Petr Janku, Ondrej Lengál, Tomás Vojnar
2017 A* conf
Register automata with linear arithmetic.
LICS
Yu-Fang Chen, Ondrej Lengál, Tony Tan, Zhilin Wu
2017 J jnl
Register automata with linear arithmetic.
CoRR
Yu-Fang Chen, Ondrej Lengál, Tony Tan, Zhilin Wu
2017 — conf
SPEN: A Solver for Separation Logic.
NFM
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, Tomás Vojnar
2016 A* conf
PAC learning-based verification and model synthesis.
ICSE
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2016 A conf
Run Forester, Run Backwards! - (Competition Contribution).
TACAS
Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
2016 J jnl
Verification of heap manipulating programs with ordered data by extended forest automata.
Acta Informatica
Parosh Aziz Abdulla, Lukás Holík, Bengt Jonsson, Ondrej Lengál, Cong Quy Trinh, Tomás Vojnar
2015 — —
Automaty v nekonečně stavové formální verifikaci ; Automata in Infinite-state Formal Verification.
Ondrej Lengál
2015 A conf
Forester: Shape Analysis Using Tree Automata - (Competition Contribution).
TACAS
Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
2015 A conf
Nested Antichains for WS1S.
TACAS
Tomás Fiedor, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2015 J jnl
Nested Antichains for WS1S.
CoRR
Tomás Fiedor, Lukás Holík, Ondrej Lengál, Tomás Vojnar
2015 J jnl
PAC Learning-Based Verification and Model Synthesis.
CoRR
Yu-Fang Chen, Chiao Hsieh, Ondrej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Farn Wang
2014 B conf
Compositional Entailment Checking for a Fragment of Separation Logic.
APLAS
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, Tomás Vojnar
2013 J jnl
Fully Automated Shape Analysis Based on Forest Automata
CoRR
Lukás Holík, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
2013 A* conf
Fully Automated Shape Analysis Based on Forest Automata.
CAV
Lukás Holík, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, Tomás Vojnar
2013 B conf
Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata.
ATVA
Parosh Aziz Abdulla, Lukás Holík, Bengt Jonsson, Ondrej Lengál, Cong Quy Trinh, Tomás Vojnar
2012 J jnl
An Efficient Finite Tree Automata Library
CoRR
Ondrej Lengál
2012 — conf
Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures.
Haifa Verification Conference
Marcela Simková, Ondrej Lengál
2012 A conf
VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata.
TACAS
Ondrej Lengál, Jirí Simácek, Tomás Vojnar
2011 B conf
Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata.
ATVA
Lukás Holík, Ondrej Lengál, Jirí Simácek, Tomás Vojnar
2011 — conf
HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware.
Haifa Verification Conference
Marcela Simková, Ondrej Lengál, Michal Kajan
2009 C conf
Methodology for Fast Pattern Matching by Deterministic Finite Automaton with Perfect Hashing.
DSD
Jan Kastil, Jan Korenek, Ondrej Lengál
2008 C conf
Network Probe for Flexible Flow Monitoring.
DDECS
Martin Zádník, Jan Korenek, Petr Kobierský, Ondrej Lengál