Detail projektu

Automaty v rozhodovacích procedurách a verifikaci

Období řešení: 1. 1. 2019 – 31. 12. 2021

Typ projektu: grant

Kód: GA19-24397S, GA19-24397S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název anglicky
Automata for Decision Procedures and Verification
Typ
grant
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.

Abstrakt

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.

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

2023

  • 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. 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Í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

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

2020

  • 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

2019

  • 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
  • Č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
  • Č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 (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.; 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.; 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.; 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
  • 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
Produkty

2019

2015

Nahoru