Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit

Poskytovatel

Ministerstvo školství, mládeže a tělovýchovy

Program

COST

Veřejná soutěž

COST 8 (SMSM2010OC5)

Hlavní účastníci

—

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

1081/2011-320

Název projektu anglicky

Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit

Anotace anglicky

The project contributes to the research planned within the COST action IC0901: Rich Model Toolkit ? An Infrastructure for Reliable Computer Systems, which is targeted at (1) development of a language for describing in a homogeneous way a broad range of computer systems to be verified and (2) research in the area of methods for formal verification with the goal of significantly increasing their generality, efficiency, and degree of automation. The proposed project in particular considers two aspects of the systems dealt with in the COST action IC0901 that constitute a very significant challenge for the current verification methods. Namely, the project considers development of new verification methods for computer systems with complex data structures (including dynamic data structures based on pointers) and/or with advanced features of concurrency. In the former case, the project concentrates on research on symbolic verification methods based on the theory of automata, logics, and their combinations.

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
(dle převodníku)

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
20206 - Computer hardware and architecture

Hodnocení poskytovatelem

V - Vynikající výsledky projektu (s mezinárodním významem atd.)

Zhodnocení výsledků projektu

Bylo zefektivněno testování inkluze nad stromovými automaty, zvýšena automatizace verifikace programů s ukazateli pomocí automatů nad lesy a navržen nový grafový přístup pro verifikaci paměťových operací velmi nízké úrovně. Testování paralelních program?

Zahájení řešení

1. 5. 2010

Ukončení řešení

31. 12. 2012

Poslední stav řešení

U - Ukončený projekt

Poslední uvolnění podpory

27. 2. 2012

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

CEP13-MSM-OC-U/01:1

Datum dodání záznamu

28. 6. 2013

Celkové uznané náklady

1 500 tis. Kč

Výše podpory ze státního rozpočtu

1 230 tis. Kč

Ostatní veřejné zdroje financování

270 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč