Publications
2026
- O. Alexaj, V. Havlena, O. Lengal, Y. Li, and N. Mazzocchi. Complementing Emerson-Lei Elevator Automata. In Proc. of 37th International Conference on Concurrency Theory — CONCUR’26, Liverpool, United Kingdom, volume 391 of LIPIcs, article 8, pages 8:1–8:22, 2026. Schloss Dagstuhl — Leibniz-Zentrum für Informatik. INCOMPLETE REFERENCE
- W. Tsai, Y. Chen, and O. Lengal. A Practical Specification Language for Automatic Quantum Program Verification. In Proc. of 38th International Conference on Computer Aided Verification — CAV’26, Lisboa, Portugal, volume 16684 of LNCS, pages 302–325, 2026. Springer-Verlag.
- O. Alexaj, V. Havlena, L. Holik, O. Lengal, Y. Li, and N. Mazzocchi. Kofola 1.0: A Modular Approach to 𝝎-Regular Complementation and Inclusion Checking. In Proc. of 38th International Conference on Computer Aided Verification — CAV’26, Lisboa, Portugal, volume 16682 of LNCS, pages 181–197, 2026. Springer-Verlag.
- V. Havlena, L. Holik, O. Lengal, J. Vasak, and S. Gulcikova. Towards Efficient Matching of Regexes with Backreferences using Register Set Automata. In Proc. of 47th ACM SIGPLAN Conference on Programming Language Design and Implementation — PLDI’26, PACMPL 10 (PLDI), Boulder, Colorado, USA, article 203, pages 855–880, 2026. ACM.
- P. A. Abdulla, Y. Chen, M. Hecko, L. Holik, O. Lengal, J. Lin, and R. S. Thinniyam. Parameterized Verification of Quantum Circuits. In Proc. of 53rd ACM SIGPLAN Symposium on Principles of Programming Languages — POPL’26, PACMPL 10 (POPL), Rennes, France, article 70, pages 2021–2050, 2026. ACM.
- 📄 preliminary version
- 📊 slides
- 🎥 video
- 🎥 video from a relevant FLAT talk
2025
- L. Holik, O. Lengal, J. Major, A. Stepkova, and J. Strejcek. On Complementation of Nondeterministic Finite Automata without Full Determinization. In Proc. of 25th International Symposium on Fundamentals of Computation Theory — FCT’25, Wroclaw, Poland, volume 16106 of LNCS, pages 221–237, 2025. Springer-Verlag.
- V. Havlena, M. Hecko, L. Holik, and O. Lengal. Negated String Containment is Decidable. In Proc. of 50th International Symposium on Mathematical Foundations of Computer Science — MFCS’25, Warsaw, Poland, volume 345 of LIPIcs, article 56, pages 56:1–56:20, 2025. Schloss Dagstuhl — Leibniz-Zentrum für Informatik.
- F. Blahoudek, Y. Chen, D. Chocholaty, V. Havlena, L. Holik, O. Lengal, and Juraj Sic. Word equations in synergy with regular constraints (extended version). Constraints 30, 1–34. 2025. Springer. 2025.
- O. Lengal. Awesome Automata: Algorithms and Applications. Habilitation thesis. FIT BUT, Brno, Czech Republic, 2025.
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. Communications of the ACM (CACM) 68(6), pages 85–93, 2025.
- Y. Chen, V. Havlena, M. Hecko, L. Holik, and O. Lengal. A Uniform Framework for Handling Position Constraints in String Solving. In Proc. of 46th ACM SIGPLAN Conference on Programming Language Design and Implementation — PLDI’25, PACMPL 9 (PLDI), Seoul, South Korea, article 169, pages 550–575, 2025. ACM.
- D. Chocholaty, V. Havlena, L. Holik, J. Hranicka, O. Lengal, and J. Sic. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In Proc. of 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’25, Hamilton, Canada, volume 15697 of LNCS, pages 23–44, 2025. Springer-Verlag.
- Y. Chen, K. Chung, M. Hsieh, W. Huang, O. Lengal, J.Lin, and W. Tsai. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. In Proc. of 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems — TACAS’25, Hamilton, Canada, volume 15698 of LNCS, pages 87–108, 2025. Springer-Verlag.
- V. Havlena, O. Lengal, and B. Smahlikova. Complementation of Emerson-Lei Automata. In Proc. of 28th International Conference on Foundations of Software Science and Computation Structures — FoSSaCS’25, Hamilton, Canada, volume 15691 of LNCS, pages 88–110, 2025. Springer-Verlag.
- 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 (POPL), Denver, Colorado, USA, article 32, pages 923–953, 2025. ACM.
- 📄 preliminary version
- 📝 technical report
- 📦 artifact
- 🛠️ AutoQ
- 📊 slides (from a VQC’25)
- 🖼️ poster
2024
- T. Chen, Y. Chen, J. Jiang, S. Jobranova, and O. Lengal. Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. In Proc. of 2024 ACM/IEEE International Conference on Computer-Aided Design — ICCAD’24, New Jersey, USA, Article No. 42, pages 1–9, 2024. ACM.
- 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.
- 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.
- 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.
- 📄 preliminary version
- 📝 technical report
- 📦 artifact
- 📊 slides
- 📚 library: Mata
- 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.
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.
- 📄 preliminary version
- 📦 artifact
- 📊 slides
- 🛠️ Z3-Noodler
- 🏆 Distinguished Paper of OOPSLA’23
- 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.
- 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 (PLDI), Orlando, Florida, USA, article 156, pages 1218–1243, 2023. ACM.
- 📄 preliminary version
- 📝 technical report
- 📦 artifact
- 🎥 video
- 📊 slides (.pptx)
- 🛠️ AutoQ
- 🏆 Distinguished Paper of PLDI’23
- 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. 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.
- 📄 preliminary version
- 📝 technical report
- 📦 artifact, (package for TACAS’23 AE VM)
- 📊 slides
- 🛠️ Kofola
- 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.
- 📄 preliminary version
- 📝 technical report
- 📊 slides
- 🛠️ Noodler
- 🏆 Best Paper of FM’23
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.
- 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.
- 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.
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.
- 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.
- 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.
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.
- 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.
- 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.
- 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.
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.
- 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.
- 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.
- 📄 preliminary version
- 📝 technical report
- 📊 slides
- 🏆 Best Paper of CADE-27
- 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.
- T. Fiedor, L. Holik, O. Lengal, and T. Vojnar. Nested Antichains for WS1S. Acta Informatica 56(3), pages 205–228, 2019. Springer-Verlag.
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.
- 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.
- 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.
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. 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
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.
- 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.
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.
- 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.
- 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.
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.
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.
- 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.
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.
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.
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.
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.