Ondřej Lengál

2024

FIEDOR Tomáš, HAVLENA Vojtěch, HOLÍK Lukáš, HRUŠKA Martin, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Mata: A Fast and Simple Finite Automata Library. In: Proceedings of TACAS'24. Luxembourgh: Springer Verlag, 2024, pp. 130-151. ISSN 0302-9743.
Detail

2023

HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software, vol. 201, no. 201, 2023, pp. 111673-111693. ISSN 0164-1212.
Detail

HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions (technical report). Ithaca: Cornell University Library, 2023.
Detail

CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao, TSAI Wei-lun and YEN Di-de. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, vol. 7, no. 6, 2023, pp. 1218-1243. ISSN 2475-1421.
Detail

CHEN Yu-Fang, CHUNG Kai-Min, LENGÁL Ondřej, LIN Jyun-ao and TSAI Wei-lun. AutoQ: An Automata-based Quantum Circuit Verifier. In: Proceedings of 35th International Conference on Computer Aided Verification. Cham: Springer Verlag, 2023, pp. 139-153. ISSN 0302-9743.
Detail

HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata. In: Proceedings of TACAS'23. Paris: Springer Verlag, 2023, pp. 249-270. ISSN 0302-9743.
Detail

HAVLENA Vojtěch, LENGÁL Ondřej, LI Yong, ŠMAHLÍKOVÁ Barbora and TURRINI Andrea. Modular Mix-and-Match Complementation of Büchi Automata (Technical Report). Ithaca: Cornell University Library, 2023.
Detail

CHEN Yu-Fang, CHOCHOLATÝ David, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and SÍČ Juraj. Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, vol. 7, no. 10, 2023, pp. 2112-2141. ISSN 2475-1421.
Detail

BLAHOUDEK František, HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej and SÍČ Juraj. Word Equations in Synergy with Regular Constraints. In: Proceedings of FM'23. Lübeck: Springer Verlag, 2023, pp. 403-423. ISSN 0302-9743.
Detail

2022

HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker. In: Proceedings of the 34th International Conference on Computer Aided Verification. Haifa: Springer Verlag, 2022, pp. 188-201. ISBN 978-3-031-13187-5. ISSN 0302-9743.
Detail

HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022.
Detail

HOLÍKOVÁ Lenka, HOLÍK Lukáš, HOMOLIAK Ivan, LENGÁL Ondřej, VEANES Margus and VOJNAR Tomáš. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In: Proceedings of the 31st USENIX Security Symposium. Boston, MA: USENIX, 2022, pp. 4165-4182. ISBN 978-1-939133-31-1.
Detail

HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation. In: Proceedings of TACAS'22. Munich: Springer Verlag, 2022, pp. 118-136. ISBN 978-3-030-99526-3. ISSN 0302-9743.
Detail

HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation (Technical Report). Ithaca, 2022.
Detail

2021

HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Automata Terms in a Lazy WSkS Decision Procedure. Journal of Automated Reasoning, vol. 65, no. 7, 2021, pp. 971-999. ISSN 0168-7433.
Detail

HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Deciding S1S: Down the Rabbit Hole and Through the Looking Glass. In: Proceedings of NETYS'21. Lecture notes in Computer Science. Cham: Springer Verlag, 2021, pp. 215-222. ISSN 0302-9743.
Detail

HAVLENA Vojtěch and LENGÁL Ondřej. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation. In: 32nd International Conference on Concurrency Theory (CONCUR 2021). Paris: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021, pp. 1-19. ISSN 1868-8969.
Detail

HAVLENA Vojtěch and LENGÁL Ondřej. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report). Ithaca, 2021.
Detail

2020

HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In: Proceedings of APLAS'20. Heidelberg: Springer Verlag, 2020, pp. 343-363. ISSN 0302-9743.
Detail

HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej, VALEŠ Ondřej and VOJNAR Tomáš. Antiprenexing for WSkS: A Little Goes a Long Way. In: EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020, pp. 298-316. ISSN 2398-7340.
Detail

ČEŠKA Milan, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. International Journal on Software Tools for Technology Transfer, vol. 22, no. 5, 2020, pp. 523-539. ISSN 1433-2779.
Detail

HOLÍKOVÁ Lenka, HOLÍK Lukáš, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus and VOJNAR Tomáš. Regex Matching with Counting-Set Automata. Proceedings of the ACM on Programming Languages, vol. 4, no. 11, 2020, pp. 1-30. ISSN 2475-1421.
Detail

2019

HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Automata Terms in a Lazy WSkS Decision Procedure. In: Proceedings of 27th International Conference on Automated Deduction (CADE-27). Natal: Springer Verlag, 2019, pp. 300-318. ISSN 0302-9743.
Detail

HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Automata Terms in a Lazy WSkS Decision Procedure (Technical Report). Ithaca, 2019.
Detail

ČEŠKA Milan, HAVLENA Vojtěch, HOLÍK Lukáš, KOŘENEK Jan, LENGÁL Ondřej, MATOUŠEK Denis, MATOUŠEK Jiří, SEMRIČ Jakub and VOJNAR Tomáš. Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. In: Proceedings - 27th IEEE International Symposium on Field-Programmable Custom Computing Machines, FCCM 2019. San Diego, CA: Institute of Electrical and Electronics Engineers, 2019, pp. 109-117. ISBN 978-1-7281-1131-5.
Detail

FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. Acta Informatica, vol. 56, no. 3, 2019, pp. 205-228. ISSN 0001-5903.
Detail

CHEN Yu-Fang, HAVLENA Vojtěch and LENGÁL Ondřej. Simulations in Rank-Based Büchi Automata Complementation. In: Proceedings of 17th Asian Symposium on Programming Languages and Systems (APLAS). Nusa Dua: Springer International Publishing, 2019, pp. 447-467. ISSN 0302-9743.
Detail

HOLÍK Lukáš, HOLÍKOVÁ Lenka, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus and VOJNAR Tomáš. Succinct Determinisation of Counting Automata via Sphere Construction. In: In Proc. of 17th Asian Symposium on Programming Languages and Systems - APLAS'19. Berlin Heidelberg: Springer Verlag, 2019, pp. 468-489. ISSN 0302-9743.
Detail

HOLÍK Lukáš, HOLÍKOVÁ Lenka, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus and VOJNAR Tomáš. Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report). Ithaca: Cornell University Library, 2019.
Detail

2018

HEIZMANN Matthias, CHEN Yu-Fang, LENGÁL Ondřej, LI Yong, TSAI Ming-Hsien, TURRINI Andrea and ZHANG Lijun. Advanced Automata-based Algorithms for Program Termination Checking. In: Proceedings of PLDI'18. Philadelphia: Association for Computing Machinery, 2018, pp. 135-150. ISBN 978-1-4503-5698-5.
Detail

ČEŠKA Milan, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In: Proceedings of TACAS'18. Thessaloniki: Springer Verlag, 2018, pp. 155-175. ISSN 0302-9743.
Detail

HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus and VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata. In: Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Heidelberg: Springer Verlag, 2018, pp. 109-125. ISBN 978-3-030-01089-8. ISSN 0302-9743.
Detail

HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus and VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca, 2018.
Detail

2017

HONG Chih-Duo, CHEN Yu-Fang, LENGÁL Ondřej, MU Shin-Cheng, SINHA Nishant and WANG Bow-Yaw. An Executable Sequential Specification for Spark Aggregation. In: Proceedings of NETYS'17. Heidelberg: Springer Verlag, 2017, pp. 421-438. ISSN 0302-9743.
Detail

HONG Chih-Duo, CHEN Yu-Fang, LENGÁL Ondřej, MU Shin-Cheng, SINHA Nishant and WANG Bow-Yaw. An Executable Sequential Specification for Spark Aggregation. Ithaca, 2017.
Detail

ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design, vol. 2017, no. 51, pp. 575-607. ISSN 0925-9856.
Detail

HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Lecture Notes in Computer Science, vol. 10145. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0. ISSN 0302-9743.
Detail

HRUŠKA Martin, HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. Brno: Faculty of Information Technology BUT, 2017.
Detail

LENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak and RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 499-517. ISBN 978-3-662-46680-3. ISSN 0302-9743.
Detail

HRUŠKA Martin, HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forester: From Heap Shapes to Automata Predicates. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10206. Heidelberg: Springer Verlag, 2017, pp. 365-369. ISBN 978-3-662-54580-5.
Detail

FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 407-425. ISBN 978-3-662-54576-8. ISSN 0302-9743.
Detail

FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. arXiv:1701.06282, 2017.
Detail

CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony and WU Zhilin. Register Automata with Linear Arithmetic. In: Proceedings of LICS'17. Reykjavik: IEEE Computer Society, 2017, pp. 1-12. ISBN 978-1-5090-3018-7.
Detail

CHEN Yu-Fang, LENGÁL Ondřej, TAN Tony and WU Zhilin. Register Automata with Linear Arithmetic. arXiv:1704.03972, 2017.
Detail

ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. SPEN: A Solver for Separation Logic. In: Proceedings of NFM'17. Lecture Notes in Computer Science, vol. 10227. Heidelberg: Springer Verlag, 2017, pp. 302-309. ISBN 978-3-319-57287-1.
Detail

2016

CHEN Yu-Fang, HSIEH Chiao, LENGÁL Ondřej, LII Tsung-Ju, TSAI Ming-Hsien, WANG Bow-Yaw and WANG Farn. PAC Learning-Based Verification and Model Synthesis. In: Proceedings of the 38th International Conference on Software Engineering. Austin, TX: Association for Computing Machinery, 2016, pp. 714-724. ISBN 978-1-4503-3900-1.
Detail

HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Run Forester, Run Backwards! (Competition Contribution). In: Proceedings of TACAS'16. Lecture Notes in Computer Science, vol. 9636. Heidelberg: Springer Verlag, 2016, pp. 923-926. ISBN 978-3-662-49673-2.
Detail

HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, SEKANINA Lukáš, VAŠÍČEK Zdeněk and VOJNAR Tomáš. Towards Formal Relaxed Equivalence Checking in Approximate Computing Methodology. In: 2nd Workshop on Approximate Computing (WAPCO 2016). Prague, 2016, pp. 1-6.
Detail

2015

HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In: Proceedings of TACAS'15. Lecture Notes in Computer Science, vol. 9035. Heidelberg: Springer Verlag, 2015, pp. 432-435. ISBN 978-3-662-46680-3.
Detail

FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Nested Antichains for WS1S. In: Proceedings of TACAS'15. Lecture Notes in Computer Science, vol. 9035. Heidelberg: Springer Verlag, 2015, pp. 658-674. ISBN 978-3-662-46680-3.
Detail

ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica, vol. 53, no. 4, 2015, pp. 357-385. ISSN 0001-5903.
Detail

2014

ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. In: Proceedings of APLAS'14. Lecture Notes in Computer Science, vol. 8858. Heidelberg: Springer Verlag, 2014, pp. 314-333. ISBN 978-3-319-12735-4.
Detail

ENEA Constantin, LENGÁL Ondřej, SIGHIREANU Mihaela and VOJNAR Tomáš. Compositional Entailment Checking for a Fragment of Separation Logic. FIT-TR-2014-01, Brno: Faculty of Information Technology BUT, 2014.
Detail

2013

HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. In: Proceedings of CAV'13. Heidelberg: Springer Verlag, 2013, pp. 740-755. ISBN 978-3-642-39798-1. ISSN 0302-9743.
Detail

HOLÍK Lukáš, LENGÁL Ondřej, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Fully Automated Shape Analysis Based on Forest Automata. FIT-TR-2013-01, Brno: Faculty of Information Technology BUT, 2013.
Detail

ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, pp. 224-239. ISBN 978-3-319-02443-1.
Detail

ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong and VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. FIT-TR-2013-02, Brno: Faculty of Information Technology BUT, 2013.
Detail

2012

LENGÁL Ondřej. An Efficient Finite Tree Automata Library: The Design of BDD-based Semi-symbolic Algorithms for Nondeterministic Finite Tree Automata. Saarbrücken: Lambert Academic Publishing, 2012. ISBN 978-3-659-27069-7.
Detail

ZACHARIÁŠOVÁ Marcela, LENGÁL Ondřej and KAJAN Michal. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. Lecture Notes in Computer Science, vol. 2012, no. 7261, pp. 247-253. ISSN 0302-9743.
Detail

ZACHARIÁŠOVÁ Marcela and LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. FIT-TR-2012-03, Brno: Faculty of Information Technology BUT, 2012.
Detail

ZACHARIÁŠOVÁ Marcela and LENGÁL Ondřej. Towards Beneficial Hardware Acceleration in HAVEN: Evaluation of Testbed Architectures. Lecture Notes in Computer Science, vol. 2013, no. 7857, 2012, pp. 266-273. ISSN 0302-9743.
Detail

LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science, vol. 2012, no. 7214, pp. 79-94. ISSN 0302-9743.
Detail

2011

HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. Lecture Notes in Computer Science, vol. 2011, no. 6996, pp. 243-258. ISSN 0302-9743.
Detail

HOLÍK Lukáš, LENGÁL Ondřej, ŠIMÁČEK Jiří and VOJNAR Tomáš. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. FIT-TR-2011-04, Brno: Faculty of Information Technology BUT, 2011.
Detail

ZACHARIÁŠOVÁ Marcela, LENGÁL Ondřej and KAJAN Michal. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. FIT-TR-2011-05, Brno: Faculty of Information Technology BUT, 2011.
Detail

2009

KAŠTIL Jan, KOŘENEK Jan and LENGÁL Ondřej. Methodology for Fast Pattern Matching by Deterministic Finite Automaton with Perfect Hashing. In: 12th EUROMICRO Conference on Digital System Design DSD 2009. Patras: IEEE Computer Society, 2009, pp. 823-289. ISBN 978-0-7695-3782-5.
Detail

2008

ŽÁDNÍK Martin, KOŘENEK Jan, LENGÁL Ondřej and KOBIERSKÝ Petr. Network Probe for Flexible Flow Monitoring. In: Proc. of 2008 IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop. Bratislava: IEEE Computer Society, 2008, pp. 213-218. ISBN 978-1-4244-2276-0.
Detail

Study Department

Ondřej Lengál

Publications