Efficient Automata Techniques for Formal Reasoning
Public support
Provider
Czech Science Foundation
Programme
Junior Grants
Call for proposals
Juniorské granty 2 (SGA0201600002)
Main participants
Vysoké učení technické v Brně / Fakulta informačních technologií
Contest type
VS - Public tender
Contract ID
16-24707Y
Alternative language
Project name in Czech
Efektivní techniky pro práci s automaty ve formálním usuzování
Annotation in Czech
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 jak rigorózní matematický popis navrhovaných metod a studium jejich teoretických vlastností, tak i jejich experimentální implementaci a vyhodnocení, na které bude kladen zvláštní důraz.
Scientific branches
R&D category
ZV - Basic research
CEP classification - main branch
IN - Informatics
CEP - secondary branch
—
CEP - another secondary branch
—
OECD FORD - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Completed project evaluation
Provider evaluation
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Project results evaluation
The main project outcomes are new techniques for formal verification of computer systems based mainly on new results in automata theory and logic. Most publications are of excellent quality (in particular, several papers were accepted to CORE Rank A* conferences). The project team included many PhD students and thus also contributed to educating a new generation of researchers.
Solution timeline
Realization period - beginning
Jan 1, 2016
Realization period - end
Nov 29, 2019
Project status
U - Finished project
Latest support payment
Apr 26, 2018
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP20-GA0-GJ-U/02:1
Data delivery date
Mar 2, 2020
Finance
Total approved costs
8,142 thou. CZK
Public financial support
8,142 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK