Publications
-
2024
HAVLENA, V.; HEČKO, M.; HOLÍK, L.; LENGÁL, O.; HABERMEHL, P. Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic. Proceedings of CAV'24. Lecture Notes in Computer Science. Montreal: Springer Verlag, 2024.
p. 42-67. ISSN: 0302-9743. DetailJOBRANOVÁ, S.; LENGÁL, O.; CHEN, T.; CHEN, Y.; JIANG, J. Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. IEEE/ACM International Conference on Computer-Aided Design (ICCAD '24), October 27--31, 2024, New York, NY, USA. Association for Computing Machinery, 2024.
p. 0-0. ISBN: 979-8-4007-1077-3. Detail -
2023
CHEN, Y.; CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Solving String Constraints with Lengths by Stabilization. Proceedings of the ACM on Programming Languages, 2023, vol. 7, no. 10,
p. 2112-2141. ISSN: 2475-1421. DetailHAVLENA, V.; CHOCHOLATÝ, D.; LENGÁL, O.; HOLÍK, L.; SÍČ, J.; BLAHOUDEK, F.; CHEN, Y. Word Equations in Synergy with Regular Constraints. In Proceedings of FM'23. Lecture Notes in Computer Science. Lübeck: Springer Verlag, 2023.
p. 403-423. ISSN: 0302-9743. DetailHAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A symbolic algorithm for the case-split rule in solving word constraints with extensions (technical report). Ithaca: Cornell University Library, 2023.
p. 0-0. DetailHAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A symbolic algorithm for the case-split rule in solving word constraints with extensions. JOURNAL OF SYSTEMS AND SOFTWARE, 2023, vol. 201, no. 201,
p. 111673-111693. ISSN: 0164-1212. DetailHAVLENA, V.; ŠMAHLÍKOVÁ, B.; LENGÁL, O.; LI, Y.; TURRINI, A. Modular Mix-and-Match Complementation of Büchi Automata (Technical Report). Ithaca: Cornell University Library, 2023.
p. 1-37. DetailHAVLENA, V.; ŠMAHLÍKOVÁ, B.; LENGÁL, O.; LI, Y.; TURRINI, A. Modular Mix-and-Match Complementation of Büchi Automata. In Proceedings of TACAS'23. Lecture Notes in Computer Science. Paris: Springer Verlag, 2023.
p. 249-270. ISSN: 0302-9743. DetailLENGÁL, O.; CHEN, Y.; TSAI, W.; CHUNG, K.; LIN, J. AutoQ: An Automata-based Quantum Circuit Verifier. In Proceedings of 35th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer Verlag, 2023.
p. 139-153. ISSN: 0302-9743. DetailLENGÁL, O.; CHEN, Y.; TSAI, W.; LIN, J.; CHUNG, K.; YEN, D. An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. Proceedings of the ACM on Programming Languages, 2023, vol. 7, no. 6,
p. 1218-1243. ISSN: 2475-1421. Detail -
2022
HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022.
p. 0-0. DetailHAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation (Technical Report). Ithaca: 2022.
p. 0-0. DetailHAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker. In Proceedings of the 34th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Haifa: Springer Verlag, 2022.
p. 188-201. ISBN: 978-3-031-13187-5. ISSN: 0302-9743. DetailHAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation. In Proceedings of TACAS'22. Lecture Notes in Computer Science. Munich: Springer Verlag, 2022.
p. 118-136. ISBN: 978-3-030-99526-3. ISSN: 0302-9743. DetailHOLÍKOVÁ, L.; HOLÍK, L.; HOMOLIAK, I.; LENGÁL, O.; VEANES, M.; VOJNAR, T. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In Proceedings of the 31st USENIX Security Symposium. Boston, MA: USENIX, 2022.
p. 4165-4182. ISBN: 978-1-939133-31-1. Detail -
2021
HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure. JOURNAL OF AUTOMATED REASONING, 2021, vol. 65, no. 7,
p. 971-999. ISSN: 0168-7433. DetailHAVLENA, V.; LENGÁL, O. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report). Ithaca: 2021.
p. 1-28. DetailHAVLENA, V.; LENGÁL, O. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics, LIPIcs. Paris: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021.
p. 1-19. ISSN: 1868-8969. DetailŠMAHLÍKOVÁ, B.; HAVLENA, V.; LENGÁL, O. Deciding S1S: Down the Rabbit Hole and Through the Looking Glass. In Proceedings of NETYS'21. Lecture Notes in Computer Science. Lecture notes in Computer Science. Cham: Springer Verlag, 2021.
p. 215-222. ISSN: 0302-9743. Detail -
2020
ČEŠKA, M.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. International Journal on Software Tools for Technology Transfer, 2020, vol. 22, no. 5,
p. 523-539. ISSN: 1433-2779. DetailHAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VALEŠ, O.; VOJNAR, T. Antiprenexing for WSkS: A Little Goes a Long Way. In EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020.
p. 298-316. ISSN: 2398-7340. DetailHAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Proceedings of APLAS'20. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2020.
p. 343-363. ISSN: 0302-9743. DetailHOLÍKOVÁ, L.; HOLÍK, L.; LENGÁL, O.; SAARIKIVI, O.; VEANES, M.; VOJNAR, T. Regex Matching with Counting-Set Automata. Proceedings of the ACM on Programming Languages, 2020, vol. 4, no. 11,
p. 1-30. ISSN: 2475-1421. Detail -
2019
CHEN, Y.; HAVLENA, V.; LENGÁL, O. Simulations in Rank-Based Büchi Automata Complementation. In Proceedings of 17th Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science. Nusa Dua: Springer International Publishing, 2019.
p. 447-467. ISSN: 0302-9743. DetailFIEDOR, T.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Nested Antichains for WS1S. Acta Informatica, 2019, vol. 56, no. 3,
p. 205-228. ISSN: 0001-5903. DetailHAVLENA, V.; ČEŠKA, M.; HOLÍK, L.; KOŘENEK, J.; LENGÁL, O.; MATOUŠEK, D.; MATOUŠEK, J.; SEMRIČ, J.; VOJNAR, T. 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.
p. 109-117. ISBN: 978-1-7281-1131-5. DetailHAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure (Technical Report). Ithaca: 2019.
p. 1-25. DetailHAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure. In Proceedings of 27th International Conference on Automated Deduction (CADE-27). Lecture Notes in Computer Science. Natal: Springer Verlag, 2019.
p. 300-318. ISSN: 0302-9743. DetailHOLÍK, L.; HOLÍKOVÁ, L.; LENGÁL, O.; VOJNAR, T.; SAARIKIVI, O.; VEANES, M. Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report). Ithaca: Cornell University Library, 2019.
p. 1-19. DetailHOLÍK, L.; HOLÍKOVÁ, L.; LENGÁL, O.; VOJNAR, T.; SAARIKIVI, O.; VEANES, M. Succinct Determinisation of Counting Automata via Sphere Construction. In In Proc. of 17th Asian Symposium on Programming Languages and Systems - APLAS'19. Lecture Notes in Computer Science. Berlin Heidelberg: Springer Verlag, 2019.
p. 468-489. ISSN: 0302-9743. Detail -
2018
ČEŠKA, M.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In Proceedings of TACAS'18. Lecture Notes in Computer Science. Thessaloniki: Springer Verlag, 2018.
p. 155-175. ISSN: 0302-9743. DetailHOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca: 2018.
p. 1-23. DetailHOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata. In Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2018.
p. 109-125. ISBN: 978-3-030-01089-8. ISSN: 0302-9743. DetailLENGÁL, O.; HEIZMANN, M.; CHEN, Y.; LI, Y.; TSAI, M.; TURRINI, A.; ZHANG, L. Advanced Automata-based Algorithms for Program Termination Checking. In Proceedings of PLDI'18. Philadelphia: Association for Computing Machinery, 2018.
p. 135-150. ISBN: 978-1-4503-5698-5. Detail -
2017
FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. arXiv:1701.06282: 2017.
p. 0-0. DetailFIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017.
p. 407-425. ISBN: 978-3-662-54576-8. ISSN: 0302-9743. DetailHOLÍK, L.; HRUŠKA, M.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In Proceedings of VMCAI'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Cham: Springer Verlag, 2017.
p. 288-309. ISBN: 978-3-319-52234-0. ISSN: 0302-9743. DetailHRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Forester: From Heap Shapes to Automata Predicates. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017.
p. 365-369. ISBN: 978-3-662-54580-5. DetailHRUŠKA, M.; HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. Brno: Faculty of Information Technology BUT, 2017.
p. 1-23. DetailLENGÁL, O.; CHEN, Y.; TAN, T.; WU, Z. Register Automata with Linear Arithmetic. arXiv:1704.03972: 2017.
p. 1-30. DetailLENGÁL, O.; CHEN, Y.; TAN, T.; WU, Z. Register Automata with Linear Arithmetic. In Proceedings of LICS'17. Reykjavik: IEEE Computer Society, 2017.
p. 1-12. ISBN: 978-1-5090-3018-7. DetailLENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B. An Executable Sequential Specification for Spark Aggregation. Ithaca: 2017.
p. 0-0. DetailLENGÁL, O.; HONG, C.; CHEN, Y.; MU, S.; SINHA, N.; WANG, B. An Executable Sequential Specification for Spark Aggregation. In Proceedings of NETYS'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017.
p. 421-438. ISSN: 0302-9743. DetailLENGÁL, O.; LIN, A.; MAJUMDAR, R.; RUMMER, P. Fair Termination for Parameterized Probabilistic Concurrent Systems. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017.
p. 499-517. ISBN: 978-3-662-46680-3. ISSN: 0302-9743. DetailLENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M. Compositional Entailment Checking for a Fragment of Separation Logic. FORMAL METHODS IN SYSTEM DESIGN, 2017, vol. 2017, no. 51,
p. 575-607. ISSN: 0925-9856. DetailLENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M. SPEN: A Solver for Separation Logic. In Proceedings of NFM'17. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017.
p. 302-309. ISBN: 978-3-319-57287-1. Detail -
2016
CHEN, Y.; HSIEH, C.; LENGÁL, O.; LII, T.; TSAI, M.; WANG, B.; WANG, F. PAC Learning-Based Verification and Model Synthesis. In Proceedings of the 38th International Conference on Software Engineering. Austin, TX: Association for Computing Machinery, 2016.
p. 714-724. ISBN: 978-1-4503-3900-1. DetailHOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; SEKANINA, L.; VAŠÍČEK, Z.; VOJNAR, T. Towards Formal Relaxed Equivalence Checking in Approximate Computing Methodology. 2nd Workshop on Approximate Computing (WAPCO 2016). Prague: 2016.
p. 1-6. DetailHRUŠKA, M.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.; HOLÍK, L.; ROGALEWICZ, A. Run Forester, Run Backwards! (Competition Contribution). In Proceedings of TACAS'16. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2016.
p. 923-926. ISBN: 978-3-662-49673-2. Detail -
2015
FIEDOR, T.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Nested Antichains for WS1S. In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015.
p. 658-674. ISBN: 978-3-662-46680-3. DetailHOLÍK, L.; LENGÁL, O.; VOJNAR, T.; JONSSON, B.; TRINH, Q.; ABDULLA, P. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica, 2015, vol. 53, no. 4,
p. 357-385. ISSN: 0001-5903. DetailHRUŠKA, M.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T.; HOLÍK, L.; ROGALEWICZ, A. Forester: Shape Analysis Using Tree Automata (Competition Contribution). In Proceedings of TACAS'15. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2015.
p. 432-435. ISBN: 978-3-662-46680-3. Detail -
2014
ENEA, C.; LENGÁL, O.; SIGHIREANU, M.; VOJNAR, T. Compositional Entailment Checking for a Fragment of Separation Logic. In Proceedings of APLAS'14. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2014.
p. 314-333. ISBN: 978-3-319-12735-4. Detail -
2013
HOLÍK, L.; JONSSON, B.; LENGÁL, O.; VOJNAR, T.; TRINH, Q.; ABDULLA, P. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013.
p. 224-239. ISBN: 978-3-319-02443-1. DetailHOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T. Fully Automated Shape Analysis Based on Forest Automata. Proceedings of CAV'13. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2013.
p. 740-755. ISBN: 978-3-642-39798-1. ISSN: 0302-9743. Detail -
2012
LENGÁL, O. 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. 64 p. ISBN: 978-3-659-27069-7. Detail
LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. VATA: A Library for Efficient Manipulation of Non-Deterministic Tree Automata. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214,
p. 79-94. ISSN: 0302-9743. DetailZACHARIÁŠOVÁ, M.; LENGÁL, O.; KAJAN, M. HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware. Lecture Notes in Computer Science, 2012, vol. 2012, no. 7261,
p. 247-253. ISSN: 0302-9743. Detail -
2011
HOLÍK, L.; LENGÁL, O.; ŠIMÁČEK, J.; VOJNAR, T. Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6996,
p. 243-258. ISSN: 0302-9743. Detail -
2009
KAŠTIL, J.; KOŘENEK, J.; LENGÁL, O. Methodology for Fast Pattern Matching by Deterministic Finite Automaton with Perfect Hashing. 12th EUROMICRO Conference on Digital System Design DSD 2009. Patras: IEEE Computer Society, 2009.
s. 823-289. ISBN: 978-0-7695-3782-5. Detail -
2008
ŽÁDNÍK, M.; KOŘENEK, J.; LENGÁL, O.; KOBIERSKÝ, P. Network Probe for Flexible Flow Monitoring. Proc. of 2008 IEEE Design and Diagnostics of Electronic Circuits and Systems Workshop. Bratislava: IEEE Computer Society, 2008.
p. 213-218. ISBN: 978-1-4244-2276-0. Detail