Detail projektu

Efficient Automata Techniques for Formal Reasoning

Období řešení: 1. 1. 2016 - 31. 12. 2018

Typ projektu: grant

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áš, doc. Mgr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Publikace

2020

2019

2018

2017

2016

Produkty

2018

2017

Nahoru