Cílem projektu je navrhnout efektivní heuristiky pro efektivní práci s různými typy automatů. Tyto techniky budou následně ověřeny v oblasti analýzy práce s pamětí, práce s řetězci a v oblasti ověřování konečnosti běhu, resp. vlastností typu živost.

Popis anglicky
As indicated already above, the essence of the project is to deliver a strong push towards unleashing the potential of automata in practice through efficient heuristics. The efficiency of the heuristics should be demonstrated by using the developed techniques to advance the state of the art in shape analysis, string analysis, and termination/liveness analysis.

Klíčová slova
Konečné automaty na konečných i nekonečných objektech, heuristiky pro efektivní operace s automaty, rozhodovací procedury, formální analýza a verifikace, analýza programů s ukazateli, analýza programů s řetězci, analýza konečnosti běhu a vlastností typu živost.

Klíčová slova anglicky
Finite on automata on finite and infinite objects, heuristics for efficient operations with automata, decision procedures, formal analysis and verification, shape analysis, string analysis, termination and liveness analysis.

GA19-24397S

čeština

Holík Lukáš, doc. Mgr., Ph.D. - hlavní řešitel
Andriushchenko Roman, Ing. - spoluřešitel
Češka Milan, doc. RNDr., Ph.D. - spoluřešitel
Havlena Vojtěch, Ing., Ph.D. - spoluřešitel
Holíková Lenka, Ing., Ph.D. - spoluřešitel
Hošták Viliam Samuel, Ing. - spoluřešitel
Hruška Martin, Ing., Ph.D. - spoluřešitel
Chocholatý David, Ing. - spoluřešitel
Janků Petr, Ing., Ph.D. - spoluřešitel
Křivka Zbyněk, Ing., Ph.D. - spoluřešitel
Lengál Ondřej, Ing., Ph.D. - spoluřešitel
Malásková Věra - spoluřešitel
Matyáš Jiří, Ing., Ph.D. - spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. - spoluřešitel
Slezáková Alexandra, Bc. - spoluřešitel
Šedý Michal, Ing. - spoluřešitel
Šoková Veronika, Ing. - spoluřešitel
Turcel Matej, Ing. - spoluřešitel
Vargovčík Pavol, Ing. - spoluřešitel
Vojnar Tomáš, prof. Ing., Ph.D. - spoluřešitel

Ústav inteligentních systémů
- odpovědné pracoviště (8.4.2018 - nezadáno)
Fakulta informatiky
- spolupříjemce (8.4.2018 - 31.12.2021)
Ústav inteligentních systémů
- příjemce (8.4.2018 - 31.12.2021)

HOLÍKOVÁ, L.; HORKÝ, M.; SÍČ, J. Automata with Bounded Repetition in RE2. In Computer Aided Systems Theory - EUROCAST 2022. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2023. p. 232-239. ISSN: 0302-9743.
Detail

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

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

HOLÍ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.
Detail

HOLÍK, L.; VARGOVČÍK, P. Simplifying Alternating Automata for Emptiness Testing. In Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings. Cham: Springer International Publishing, 2021. p. 243-264. ISBN: 978-3-030-89051-3.
Detail

HOLÍK, L.; HRUŠKA, M. Towards Efficient Shape Analysis with Tree Automata. In Proceedings International Conference on Networked Systems. Lecture Notes in Computer Science. Lecture notes in Computer Science. Cham: Springer Verlag, 2021. p. 206-214. ISSN: 0302-9743.
Detail

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

KÖVÁRI, A.; KŘIVKA, Z.; MEDUNA, A. Evaluating Yona Language. In INTERNATIONAL CONFERENCES ON WWW/INTERNET 2021 AND APPLIED COMPUTING 2021. Lisabon: International Association for Development of the Information Society, 2021. p. 101-108. ISBN: 978-989-8704-34-4.
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

MATYÁŠ, J.; PANKUCH, A.; VOJNAR, T.; ČEŠKA, M.; ČEŠKA, M. Approximating Complex Arithmetic Circuits with Guaranteed Worst-Case Relative Error. In International Conference on Computer Aided Systems Theory (EUROCAST'19). Lecture Notes in Computer Science. Cham: Springer Verlag, 2020. p. 482-490. ISBN: 978-3-030-45092-2.
Detail

HOLÍ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

ČEŠKA, M.; KŘETÍNSKÝ, J. Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract). In Proceedings of the 17th International Conference on Computational Methods in Systems Biology. Lecture Notes in Bioinformatics. Trieste: Springer International Publishing, 2019. p. 337-341. ISBN: 978-3-030-31303-6.
Detail

ČEŠKA, M.; HENSE, C.; JANSEN, N.; JUNGES, S.; KATOEN, J. Model Repair Revamped - On the Automated Synthesis of Markov Chains -. In From Reactive Systems to Cyber-Physical Systems. Lecture Notes of Computer Science. Cham: Springer International Publishing, 2019. p. 107-125. ISBN: 978-3-030-31513-9.
Detail

ABDULLA, P.; ATIG, M.; BUI PHI, D.; HOLÍK, L.; JANKŮ, P. Chain-Free String Constraints. In Proceedings of ATVA'19. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2019. p. 277-293. ISBN: 978-3-030-31783-6.
Detail

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

ČEŠKA, M.; HENSE, C.; JUNGES, S.; KATOEN, J. Counterexample-Driven Synthesis for Probabilistic Program Sketches. In Proceedings of the 23rd International Symposium on Formal Methods. Lecture Notes of Computer Science. Porto: Springer International Publishing, 2019. p. 101-120. ISBN: 978-3-030-30941-1.
Detail

ČEŠKA, M.; KŘETÍNSKÝ, J. Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks. In Proceedings of the 31th International Conference on Computer Aided Verification (CAV'19). Lecture Notes of Computer Science. New York: Springer International Publishing, 2019. p. 475-496. ISBN: 978-3-030-25540-4.
Detail

HOLÍK, L.; ABDULLA, P.; ATIG, M.; CHEN, Y.; REZINE, A.; STENMAN, J.: Norn; Norn: An SMT Solver for String Constraints. http://user.it.uu.se/~jarst116/norn/. URL: http://user.it.uu.se/~jarst116/norn/. (software)
Detail

HOLÍK, L.; ABDULLA, P.; ATIG, M.; BUI PHI, D.; CHEN, Y.; REZINE, A.; RUMMER, P.: Trau; Trau: SMT solver for string constraints. https://github.com/diepbp/Trau. URL: https://github.com/diepbp/Trau. (software)
Detail

Odpovědnost: Holík Lukáš, doc. Mgr., Ph.D.