Publications

2025

• P. A. Abdulla, Y. Chen, Y. Chen, L. Holik, O. Lengal, J. Lin, F. Lo, and W. Tsai. Verifying Quantum Circuits with Level-Synchronized Tree Automata. In Proc. of 52nd ACM SIGPLAN Symposium on Principles of Programming Languages — POPL’25, PACMPL 9 (32), Denver, Colorado, USA, pages 923–953, 2025. ACM. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2410.18540, 2024. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.13957472. The tool AutoQ is available at GitHub.

2024

• T. Chen, Y. Chen, J. Jiang, S. Jobranova, and O. Lengal. Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. To appear in Proc. of 2024 ACM/IEEE International Conference on Computer-Aided Design — ICCAD’24, New Jersey, USA, pages XXX–XXX, 2024. ACM. A preliminary version is available here. The slides from the presentation are available here. The tool Medusa is available at GitHub. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.13243595. INCOMPLETE REFERENCE

• V. Havlena, L. Holik, O. Lengal, and J. Sic. Cooking String-Integer Conversions with Noodles. In Proc. of 27th International Conference on Theory and Applications of Satisfiability Testing — SAT’24, Pune, India, volume 305 of LIPIcs, article 14, pages 14:1–14:19, 2024. Schloss Dagstuhl — Leibniz-Zentrum für Informatik. A preliminary version is available here. The slides from the presentation are available here.

• P. Habermehl, V. Havlena, M. Hecko, L. Holik, and O. Lengal. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. In Proc. of 36th International Conference on Computer Aided Verification — CAV’24, Montreal, Canada, volume 14681 of LNCS, pages 42–67, 2024. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2403.18995, 2024. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.10993434. The slides from the presentation are available here. The tool Amaya is available at GitHub and at DockerHub.

• D. Chocholaty, T. Fiedor, V. Havlena, L. Holik, M. Hruska, O. Lengal, and J. Sic. Mata: A Fast and Simple Finite Automata Library. In Proc. of 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’24, Luxembourg City, Luxembourg, volume 14571 of LNCS, pages 130–151, 2024. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2310.10136, 2023. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.10044515. The slides from the presentation are available here. The library Mata is available at GitHub.

• Y. Chen, D. Chocholaty, V. Havlena, L. Holik, O. Lengal, and J. Sic. Z3-Noodler: An Automata-based String Solver. In Proc. of 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’24, Luxembourg City, Luxembourg, volume 14570 of LNCS, pages 24–33, 2024. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2310.08327, 2023. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.10034513. The slides from the presentation are available here. The tool Z3-Noodler is available at GitHub.

2023

• Y. Chen, D. Chocholaty, V. Havlena, L. Holik, O. Lengal, and J. Sic. Solving String Constraints with Lengths by Stabilization. In Proc. of the ACM on Programming Languages — OOPSLA’23 issue (for Object-Oriented Programming, Systems, Languages, and Applications), volume 7 of PACMPL (number OOPSLA2), article number 296, 2023. ACM. A preliminary version is available here. Distinguished Paper of OOPSLA’23. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.8289595. The slides from the presentation are available here. The tool Z3-Noodler is available at GitHub.

• Y. Chen, K. Chung, O. Lengal, J. Lin, and W. Tsai. AutoQ: An Automata-based Quantum Circuit Verifier. In Proc. of 35th International Conference on Computer Aided Verification — CAV’23, Paris, France, volume 13966 of LNCS, pages 139–153, 2023. Springer-Verlag. A preliminary version is available here. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.7966542. The tool AutoQ is available at GitHub.

• Y. Chen, K. Chung, O. Lengal, J. Lin, W. Tsai, and D. Yen. An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits. In Proc. of 44th ACM SIGPLAN Conference on Programming Language Design and Implementation — PLDI’23, PACMPL 7 (156), Orlando, Florida, USA, pages 1218–1243, 2023. ACM. A preliminary version is available here. Distinguished Paper of PLDI’23. An extended version appeared as the technical report CoRR abs/2301.07747, 2023. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.7707349. A video with the presentation is available here. The slides from the presentation are available here (.pptx). The tool AutoQ is available at GitHub.

• Y. Chen, V. Havlena, O. Lengal, and A. Turrini. A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions. Journal of Systems and Software (JSS) 201, 111673. Elsevier. An extended version appeared as the technical report CoRR abs/2303.01142, 2023.

• V. Havlena, O. Lengal, Y. Li, B. Smahlikova, and A. Turrini. Modular Mix-and-Match Complementation of Büchi automata. In Proc. of 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’23, Paris, France, volume 13993 of LNCS, pages 249–270, 2023. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2301.01890, 2023. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.7505280 as a package for the TACAS’23 AE VM available here. The slides from the presentation are available here. The tool Kofola is available at GitHub.

• F. Blahoudek, Y. Chen, D. Chocholaty, V. Havlena, L. Holik, O. Lengal, and J. Sic. Word Equations in Synergy with Regular Constraints. In Proc. of Formal Methods - 25th International Symposium — FM’23, Lübeck, Germany, volume 14000 of LNCS, pages 403–423, 2023. Springer-Verlag. A preliminary version is available here. Best Paper of FM’23. An extended version appeared as the technical report CoRR abs/2212.02317, 2022. The slides from the presentation are available here. The tool Noodler is available at GitHub.

2022

• V. Havlena, O. Lengal, and B. Smahlikova. Complementing Büchi Automata with Ranker. In Proc. of 34th International Conference on Computer Aided Verification — CAV’22, Haifa, Israel, volume 13372 of LNCS, pages 188–201, 2022. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2206.01946, 2022. The slides from the presentation are available here. The artifact for the paper is available at Zenodo as a virtual machine under the DOI 10.5281/zenodo.6524909 and as a package that can be installed on other systems under the DOI https://doi.org/10.5281/zenodo.6525219 (the artifact is also versioned on GitHub). The tool Ranker is available at GitHub and the evaluation environment is also at GitHub.

• L. Turonova, L. Holik, I. Homoliak, O. Lengal, M. Veanes, and T. Vojnar. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In Proc. of 31st USENIX Security Symposium — USENIX-Security’22, Boston, MA, USA, pages 4165–4182, 2022. USENIX Association. A preliminary version is available here. The slides from the presentation are available here. A video with the presentation is available here.

• V. Havlena, O. Lengal, and B. Smahlikova. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation. In Proc. of 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’22, Munich, Germany, volume 13244 of LNCS, pages 118–136, 2022. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2110.10187, 2021. The slides from the presentation are available here.

2021

• V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Automata Terms in a Lazy WSkS Decision Procedure. Journal of Automated Reasoning (JAR) 65(7), pages 971–999, 2021. Springer-Verlag. A preliminary version is available here.

• V. Havlena and O. Lengal. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation. In Proc. of 32nd International Conference on Concurrency Theory — CONCUR’21, virtual conference, volume 203 of LIPIcs, article 2, pages 2:1–2:19, 2021. Schloss Dagstuhl — Leibniz-Zentrum für Informatik. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/2010.07834, 2020. The slides from the presentation are available here. A video teaser is available here. A video with the presentation is available here.

• V. Havlena, O. Lengal, and B. Smahlikova. Deciding S1S: Down the Rabbit Hole and Through the Looking Glass. In Proc. of 9th International Conference of NETworked sYStems — NETYS’21, virtual conference, volume 12754 of LNCS, pages 215–222, 2021. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. A video with the presentation is available here.

2020

• Y. Chen, V. Havlena, O. Lengal, and A. Turrini. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Proc. of the 18th Asian Symposium on Programming Languages and Systems — APLAS’20, Fukuoka, Japan, volume 12470 of LNCS, pages 343–363, 2020. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here.

• L. Turonova, L. Holik, O. Lengal, O. Saarikivi, M. Veanes, and T. Vojnar. Regex Matching with Counting-Set Automata . In Proc. of the ACM on Programming Languages — OOPSLA’20 issue (for Object-Oriented Programming, Systems, Languages, and Applications), volume 4 of PACMPL, article number 218, 2020. ACM. A preliminary version is available here. A recording of the talk is available here. An extended version appeared as the technical report MSR-TR-2020-31, Microsoft, 2020. The artifact for the paper is available at Zenodo under the DOI 10.5281/zenodo.3975566 and the data set is available at Zenodo under the DOI 10.5281/zenodo.3974360.

• M. Ceska, V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Approximate reduction of finite automata for high-speed network intrusion detection. International Journal on Software Tools for Technology Transfer (STTT) 22(5), pages 523–539, 2020. Springer-Verlag. A preliminary version is available here.

• V. Havlena, L. Holik, O. Lengal, O. Vales, and T. Vojnar. Antiprenexing for WSkS: A Little Goes a Long Way. In Proc. of the 23rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning — LPAR-23, volume 73 of EPiC, pages 298–316, 2020. Easychair. A preliminary version is available here.

2019

• L. Holik, O. Lengal, O. Saarikivi, L. Turonova, M. Veanes, and T. Vojnar. Succinct Determinisation of Counting Automata via Sphere Construction. In Proc. of the 17th Asian Symposium on Programming Languages and Systems — APLAS’19, Nusa Dua, Bali, Indonesia, volume 11893 of LNCS, pages 468–489, 2019. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report CoRR abs/1910.01996, 2019.

• Y. Chen, V. Havlena, and O. Lengal. Simulations in Rank-Based Büchi Automata Complementation. In Proc. of the 17th Asian Symposium on Programming Languages and Systems — APLAS’19, Nusa Dua, Bali, Indonesia, volume 11893 of LNCS, pages 447–467, 2019. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/1905.07139, 2019. The slides from the presentation are available here.

• V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Automata Terms in a Lazy WSkS Decision Procedure. In Proc. of the 27th International Conference on Automated Deduction — CADE-27, Natal, Brazil, volume 11716 of LNAI, pages 300–318, 2019. Springer-Verlag. A preliminary version is available here. Best Paper of CADE-27. An extended version appeared as the technical report CoRR abs/1905.08697, 2019. The slides from the presentation are available here.

• M. Ceska, V. Havlena, L. Holik, J. Korenek O. Lengal, D. Matousek, J. Matousek, J. Semric, and T. Vojnar. Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. In Proc. of 27th IEEE International Symposium On Field-Programmable Custom Computing Machines — FCCM’19, San Diego, USA, pages 109–117, 2019. IEEE. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report CoRR abs/1904.10786.

• T. Fiedor, L. Holik, O. Lengal, and T. Vojnar. Nested Antichains for WS1S. Acta Informatica 56(3), pages 205–228, 2019. Springer-Verlag. A preliminary version is available here. The associated tool dWiNA is available here.

2018

• L. Holik, O. Lengal, J. Sic, M. Veanes, and T. Vojnar. Simulation Algorithms for Symbolic Automata. In Proc. of 16th International Symposium on Automated Technology for Verification and Analysis — ATVA’18, Los Angeles, USA, volume 11138 of LNCS, pages 109–125, 2018. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/1807.08487, 2018.

• Y. Chen, M. Heizmann, O. Lengal, Y. Li, M. Tsai, A. Turrini, and L. Zhang. Advanced Automata-based Algorithms for Program Termination Checking. In Proc. of 39th ACM SIGPLAN Conference on Programming Language Design and Implementation — PLDI’18, Philadelphia, PA, USA, pages 135–150, 2018. ACM. A preliminary version is available here.

• M. Ceska, V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In Proc. of 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’18, Thessaloniki, Greece, volume 10806 of LNCS, pages 155–175, 2018. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report CoRR abs/1710.08647, 2018.

2017

• C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design 51(3), pages 575–607, 2017. A preliminary version is available here. Springer-Verlag.

• Y. Chen, O. Lengal, T. Tan, and Z. Wu. Register Automata with Linear Arithmetic. In Proc. of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science — LICS’17, Reykjavik, Iceland, pages 1–12, 2017. IEEE. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/1704.03972, 2017.

• C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. SPEN: A Solver for Separation Logic. In Proc. of 9th NASA Formal Methods Symposium — NFM’17, NASA Ames Research Center, Moffett Field, CA, USA, volume 10227 of LNCS,pages 302–309, 2017. Springer-Verlag. A preliminary version is available here.

• Y. Chen, C. Hong, O. Lengal, S. Mu, N. Sinha, and B. Wang. An Executable Sequential Specification for Spark Aggregation. In Proc. of 5th International Conference of NETworked sYStems — NETYS’17, Marrakech, Morocco, volume 10299 of LNCS, pages 421–438, 2017. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report CoRR abs/1702.02439, 2017.

• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Forester: From Heap Shapes to Automata Predicates (Competition Contribution). In Proc. of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’17, Uppsala, Sweden, volume 10206 of LNCS, pages 365–369, 2017. Springer-Verlag. A preliminary version is available here.

• O. Lengal, A.W. Lin, R. Majumdar, and P. Ruemmer. Fair Termination for Parameterized Probabilistic Concurrent Systems. In Proc. of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’17, Uppsala, Sweden, volume 10205 of LNCS, pages 499–517, 2017. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report CoRR abs/1710.10756, 2017.

• T. Fiedor, L. Holik, P. Janku, O. Lengal, and T. Vojnar. Lazy Automata Techniques for WS1S. In Proc. of 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’17, Uppsala, Sweden, volume 10205 of LNCS, pages 407–425, 2017. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report CoRR abs/1701.06282, 2017. The slides from the presentation are available here. The associated tool Gaston is available here.

• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, and T. Vojnar. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In Proc. of 18th International Conference on Verification, Model Checking, and Abstract Interpretation — VMCAI’17, Paris, France, volume 10145 of LNCS, pages 288–309, 2017. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2016-03, FIT BUT, Brno, Czech Republic, 2016

2016

• Y. Chen, C. Hsieh, O. Lengal, T. Lii, M. Tsai, B. Wang, and F. Wang. PAC Learning-Based Verification and Model Synthesis. In Proc. of 38th International Conference on Software Engineering — ICSE’16, Austin, Texas, pages 714–724, 2016. ACM. A preliminary version is available here.

• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Run Forester! Run Backwads! (Competition Contribution). In Proc. of 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’16, Eindhoven, Netherlands, volume 9636 of LNCS, pages 923–926, 2016. Springer-Verlag. A preliminary version is available here.

2015

• O. Lengal. Automata in Infinite-State Formal Verification. Ph.D. thesis (an abridged version). FIT BUT, Brno, Czech Republic, 2015.

• P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T. Vojnar. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Acta Informatica 53(4), pages 357–385, 2016. Springer-Verlag. A preliminary version is available here.

• T. Fiedor, L. Holik, O. Lengal, and T. Vojnar. Nested Antichains for WS1S. In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’15, London, United Kingdom, volume 9035 of LNCS, pages 658–674, 2015. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report FIT-TR-2014-06, FIT BUT, Brno, Czech Republic, 2014. The associated tool dWiNA is available here.

• L. Holik, M. Hruska, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In Proc. of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’15, London, United Kingdom, volume 9035 of LNCS, pages 431–434, 2015. Springer-Verlag. A preliminary version is available here.

2014

• C. Enea, O. Lengal, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. In Proc. of 12th Asian Symposium on Programming Languages and Systems — APLAS’14, Singapore, Singapore, volume 8858 of LNCS, pages 314–333, 2014. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report FIT-TR-2014-01, FIT BUT, Brno, Czech Republic, 2014.

2013

• P.A. Abdulla, L. Holik, B. Jonsson, O. Lengal, C.Q. Trinh, and T. Vojnar. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In Proc. of 11th International Symposium on Automated Technology for Verification and Analysis — ATVA’13, Hanoi, Vietnam, volume 8172 of LNCS, pages 224–239, 2013. Springer-Verlag. A preliminary version is available here. An extended version appeared as the technical report FIT-TR-2013-02, FIT BUT, Brno, Czech Republic, 2013.

• L. Holik, O. Lengal, A. Rogalewicz, J. Simacek, and T. Vojnar. Fully Automated Shape Analysis Based on Forest Automata. In Proc. of 25th International Conference on Computer Aided Verification — CAV’13, Saint Petersburg, Russia, volume 8044 of LNCS, pages 740–755, 2013. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here.

2012

• O. Lengal, J. Simacek, and T. Vojnar. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. In Proc. of 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’12, Tallinn, Estonia, volume 7214 of LNCS, pages 79–94, 2012. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here.

2011

• L. Holik, O. Lengal, J. Simacek, and T. Vojnar. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. In Proc. of 9th International Symposium on Automated Technology for Verification and Analysis — ATVA’11, Taipei, Taiwan, volume 6996 of LNCS, pages 243–258, 2011. Springer-Verlag. A preliminary version is available here. The slides from the presentation are available here. An extended version appeared as the technical report FIT-TR-2011-04, FIT BUT, Brno, Czech Republic, 2011.

2010

• O. Lengal. An Efficient Finite Tree Automata Library. Master’s thesis. FIT BUT, Brno, Czech Republic, 2010.

2009

• J. Kastil, J. Korenek, and O. Lengal. Methodology for Fast Pattern Matching by Deterministic Finite Automaton with Perfect Hashing. In Proc. of 12th Euromicro Conference on Digital System Design, Architectures, Methods and Tools — DSD’09, Patras, Greece, 2009. IEEE. A preliminary version is available here.

2008

• M. Zadnik, J. Korenek, P. Kobiersky, and O. Lengal. Network Probe for Flexible Flow Monitoring. In Proc. of 2008 IEEE Workshop on Design and Diagnostics of Electronic Circuits and Systems — DDECS’08, Bratislava, Slovakia, pages 213–218, 2008. IEEE. A preliminary version is available here.