Go to main content | Go to main menu | Go to search

Project information
Correctness Analysis of C and C++ Programs with Threads

Information

This project doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official project website can be found on muni.cz.
Investor logo
Project Identification
GA15-08772S
Project Period
3/2015 - 12/2017
Investor / Pogramme / Project type
Czech Science Foundation
  • Standard Projects
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

2018

2017

2016

Previous 1 2 Next

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