Analýza korektnosti vícevláknových programů v C a C++
Cíle projektu
Projekt se zaměřuje na výzkum a vývoj nových algoritmů a datových struktur, které umožní efektivní verifikaci vícevláknových programů zapsaných v programovacích jazycích C a C++ metodou ověřování modelu (angl. model checking). Konkrétním cílem projektu je vyvinout nové metody automatické abstrakce programů vstupujících do procesu verifikace, které budou realizované formou transformace těchto programů. Dále pak získat nové metody umožňující kombinaci explicitního a symbolického přístupu k verifikaci metodou ověřování modelu, či metody umožňující jiným způsobem redukovat prostorové nároky verifikačních nástrojů. Pro účely porovnání a vyhodnocení budou nově vyvinuté algoritmy a datové struktury integrovány do experimentálního softwarového nástroje DIVINE. To mimo jiné umožní efektivní využití stávajících výpočetních architektur (více-jádrové počítače, výpočetní klastry) tak, aby byla významně posunuta hranice systémů, jež je možné verifikovat automatizovanými metodami formální verifikace.
Klíčová slova
formal verificationliner temporal logicparallel and distributed model checkingLLVM bitcode
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
Standardní projekty 19 (SGA0201500001)
Hlavní účastníci
Masarykova univerzita / Fakulta informatiky
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
15-08772S
Alternativní jazyk
Název projektu anglicky
Correctness Analysis of C and C++ Programs with Threads
Anotace anglicky
The goal of this project is to research and develop new algorithms and data structures to support model checking of multi-threaded programs written in the C and C++ programming languages. The particular goals of the project include the development of new techniques for automated program abstraction by means of program transformation, techniques for efficient combination of explicit and symbolic approaches to model checking. We will also seek additional techniques for reducing memory requirements of formal verification tools, model checkers in particular. The newly developed data structures and algorithms will be implemented and evaluated within the context of the parallel LTL model checker DIVINE. Our intent is to push the tractability frontier in the area of multi-threaded C and C++ programs, taking advantage of contemporary computational platforms such as multi-core workstations or high-performance clusters.
Vědní obory
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
(dle převodníku)10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
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řináší nové výsledky v oblasti automatizované formální verifikace metodou ověřování modelu publikované ve 12 konferenčních a 3 časopiseckých (Jimp) článcích přijatelné kvality. Navržené metody byly implementovány v rámci nástroje DIVINE a experimentálně zanalyzovány. Studenti různých studijních programů byli do projektu aktivně zapojováni. Finance byly čerpány účelně.
Termíny řešení
Zahájení řešení
1. 1. 2015
Ukončení řešení
31. 12. 2017
Poslední stav řešení
U - Ukončený projekt
Poslední uvolnění podpory
5. 4. 2017
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
CEP18-GA0-GA-U/02:1
Datum dodání záznamu
4. 5. 2018
Finance
Celkové uznané náklady
4 998 tis. Kč
Výše podpory ze státního rozpočtu
4 998 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
4 998 tis. Kč
Statní podpora
4 998 tis. Kč
100%
Poskytovatel
Grantová agentura České republiky
CEP
IN - Informatika
Doba řešení
01. 01. 2015 - 31. 12. 2017