Project information
Correctness Analysis of C and C++ Programs with Threads
- 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
2016
-
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration
Model Checking Software, year: 2016
-
Weak Memory Models as LLVM-to-LLVM Transformations
Mathematical and Engineering Methods in Computer Science - 10th International Doctoral Workshop, year: 2016
2015
-
Fast, Dynamically-Sized Concurrent Hash Table
Model Checking Software, year: 2015
-
Language Emptiness of Continuous-Time Parametric Timed Automata
Automata, Languages, and Programming, year: 2015
-
Techniques for Memory-Efficient Model Checking of C and C++ Code
Software Engineering and Formal Methods, year: 2015