Publications

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, 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, 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.