Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
Standardní projekty 13 (SGA02010GA-ST)
Hlavní účastníci
—
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
P103-10-0306
Alternativní jazyk
Název projektu anglicky
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
Anotace anglicky
Automated verification of programs is currently a very hot issue due to the rising influence of computer-controlled systems on our lives and the recognised need to minimise the number of errors in them. The project, in particular, considers verificationof programs with advanced features of concurrency and unboundedness, which both belong among especially problematic features to be dealt with in automated verification. In the former case, the project pays a special attention to verification of applications intended to run on the current multi-core processors. In the latter case, verification of programs manipulating different unbounded structures, notably (parameterised-size) arrays and complex dynamic linked data structures (such as lists or trees), is considered. The project contains research on methods of dynamic as well as static verification, including model checking, and possibly their suitable combinations. For handling infinite-state programs, efficient symbolic verification methods based on automata and logics are the primary target of the research in the project.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
CEP - hlavní obor
JC - Počítačový hardware a software
CEP - vedlejší obor
IN - Informatika
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)<br>20206 - Computer hardware and architecture
Hodnocení dokončeného projektu
Hodnocení poskytovatelem
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Zhodnocení výsledků projektu
Projekt přinesl mezinárodně významné výsledky ve formální verifikaci programů s různými zdroji neomezenosti a paralelních programů. Těmi byly vysoce kvalitní publikace v časopisech (7) a na mezinárodních konferencích (31), jakož i veřejně dostupné softw?
Termíny řešení
Zahájení řešení
1. 1. 2010
Ukončení řešení
31. 12. 2013
Poslední stav řešení
U - Ukončený projekt
Poslední uvolnění podpory
12. 6. 2013
Dodání dat do CEP
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
CEP14-GA0-GA-U/01:1
Datum dodání záznamu
1. 7. 2014
Finance
Celkové uznané náklady
4 752 tis. Kč
Výše podpory ze státního rozpočtu
4 752 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč