Fakulta informačních technologií VUT v Brně

Detail projektu

Efficient Automata Techniques for Formal Reasoning

Období řešení: 01.01.2016 - 31.12.2018

Kód: GJ16-24707Y

Agentura: Grantová agentura České republiky

Program: Juniorské granty

Název česky
Efektivní automaty pro formální rozhodování
Typ
grant
Klíčová slova
konečné automaty
formální verifikace
logiky
rozhodovací procedury
programy s řetězci
paralelní programy
ukazatelové programy
bezkontextové jazyky
SAT
SMT
Abstrakt
Projekt si klade za cíl vyvinout nové efektivní a praktické algoritmy pro konečné automaty aplikovatelné ve formální verifikaci a analýze dynamických systémů. Bude stavět zejména na studiu souvislostí mezi automatovými problémy, metodami řešení SAT/SMT problémů a formální verifikací. Věříme, že hlubší porozumění spojitostí mezi metodami používanými v těchto oblastech posune vpřed nejen oblast automatových technik s aplikacemi ve verifikaci, ale také ostatní zmíněné oblasti. Vyvíjené algoritmy budou konkrétně zaměřeny zejména na aplikace automatů v analýze programů s řetězci, verifikaci programů s ukazateli, analýze paralelních programů a v rozhodovacích procedurách logik souvisejících s formální verifikací nekonečně stavových systémů, jako jsou WSkS nebo separační logika. Práce na projektu zahrne rigorózní matematický popis navrhovaných metod a studium jejich teoretických vlastností, ale také jejich experimentální implementaci a vyhodnocení.
Řešitelé
Holík Lukáš, Mgr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Češka Milan, RNDr., Ph.D. (UITS FIT VUT)
Fiedor Tomáš, Ing. (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)
Síč Juraj, Bc. (FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
Publikace

2019

2018

2017

2016

Produkty

2018

2017

Nahoru