Project information

Correctness Analysis of C and C++ Programs with Threads

Investor logo
Project Identification
GA15-08772S
Project Period
3/2015 - 12/2017
Investor / Pogramme / Project type
Czech Science Foundation
MU Faculty or unit
Faculty of Informatics

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 učely porovnání a vyhodnocení budou nově vyvinuté algoritmy a datové struktury integrovány do experimentálního softwarového nástroje DIVINE. To mimojiné 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é doposud verifikovat automatizovanými metodami formální verifikace.

Publications

Total number of publications: 15


Previous 1 2 Next

You are running an old browser version. We recommend updating your browser to its latest version.

More info