Detail projektu

Automaty v rozhodovacích procedurách a verifikaci

Období řešení: 1.1.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)
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
  • ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš a JANKŮ Petr. Chain-Free String Constraints. In: Proceedings of ATVA'19. Lecture Notes in Computer Science, roč. 11781. Cham: Springer International Publishing, 2019, s. 277-293. ISBN 978-3-030-31783-6. 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
  • HAVLENA Vojtěch, CHEN Yu-Fang a 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, s. 447-467. ISSN 0302-9743. 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
Nahoru