Efektivní techniky pro práci s automaty ve formálním usuzování

Poskytovatel
Grantová agentura České republiky
Program
Juniorské granty
Veřejná soutěž
Juniorské granty 2 (SGA0201600002)
Hlavní účastníci
Vysoké učení technické v Brně / Fakulta informačních technologií
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
16-24707Y

Název projektu anglicky
Efficient Automata Techniques for Formal Reasoning
Anotace anglicky
The project focuses on development of efficient algorithms for finite automata applicable in formal verification and analysis of dynamic systems. The central idea is to explore connections between automata, SAT/SMT solving, and program verification. We believe that because all these three domains solve similar problems, interchanging ideas between the domains is possible and may significantly advance not only the domain of automata but also the other mentioned areas. The automata-based algorithms developed in the project will in particular target the following four lively domains of applications: analysis of string manipulating programs, shape analysis, verification of concurrent programs, and decision procedures of selected logics suitable for verification of infinite-state systems (such as WSkS or separation logic). The work on the project will include rigorous mathematical description of the developed principles and algorithms, as well as their implementation and experimental evaluation, which will be emphasized.

Kategorie VaV
ZV - Základní výzkum
CEP - hlavní obor
IN - Informatika
CEP - vedlejší obor
—
CEP - další vedlejší obor
—
OECD FORD - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Hodnocení poskytovatelem
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Zhodnocení výsledků projektu
Výsledkem projektu jsou nové poznatky a techniky použitelné pro formální verifikaci počítačových systémů založené na nových výsledcích v oblasti teorie automatů a temporálních logik. Většina publikací, které v rámci projektu vznikly, má špičkovou kvalitu (příslušné konference mají CORE Rank A* nebo A). Do práce byla zapojena řada doktorských studentů.

Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP20-GA0-GJ-U/02:1
Datum dodání záznamu
2. 3. 2020

Podobné projekty(10)