Detail projektu
Automaty v rozhodovacích procedurách a verifikaci
Období řešení: 01.01.2019 - 31.12.2021
Kód: 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áš, Mgr., Ph.D.
(UITS FIT VUT)
, hlavní řešitel
Strejček Jan, doc. RNDr., Ph.D. (FI MUNI) , spoluřešitel
Češka Milan, RNDr., Ph.D. (UITS FIT VUT)
Havlena Vojtěch, Ing. (UITS FIT VUT)
Hruška Martin, Ing. (UITS FIT VUT)
Janků Petr, Ing. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Matyáš Jiří, Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
Vargovčík Pavol, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Strejček Jan, doc. RNDr., Ph.D. (FI MUNI) , spoluřešitel
Češka Milan, RNDr., Ph.D. (UITS FIT VUT)
Havlena Vojtěch, Ing. (UITS FIT VUT)
Hruška Martin, Ing. (UITS FIT VUT)
Janků Petr, Ing. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Matyáš Jiří, Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
Vargovčík Pavol, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Publikace
2019
- ČEŠKA Milan, HENSE Christian, JUNGES Sebastian a KATOEN Joost-Pieter. Counterexample-Driven Synthesis for Probabilistic Program Sketches. In: Proceedings of the 23rd International Symposium on Formal Methods. To be published in 2019. Porto: Springer International Publishing, 2019, s. 1-19. Detail
- ČEŠKA Milan a KŘETÍNSKÝ Jan. 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, s. 475-496. ISBN 978-3-030-25540-4. Detail
- ČEŠKA Milan a KŘETÍNSKÝ Jan. Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract). In: Proceedings of the 17th International Conference on Computational Methods in Systems Biology (CMSB'19). To be published in 2019. Trieste: Springer International Publishing, 2019, s. 1-4. Detail
Produkty
2019
- Trau: SMT řešič řetězcových omezení, software, 2019
Autoři: Abdulla Parosh A., Atig Mohamed F., Bui Phi Diep, Holík Lukáš, Chen Yu-Fang, Rezine Ahmed, Rummer Philipp Detail
2015
- Norn: SMT řešič řetězcových omezení, software, 2015
Autoři: Abdulla Parosh A., Atig Mohamed F., Holík Lukáš, Chen Yu-Fang, Rezine Ahmed, Stenman Jari Detail