Project information
Project information
Verifikace MPI programů pomocí DIVINE
- Project Identification
- MUNI/33/01/2015
- Project Period
- 4/2015 - 12/2015
- Investor / Pogramme / Project type
-
Masaryk University
- FI Dean's Programme
- MU Faculty or unit
-
Faculty of Informatics
- Mgr. Marek Tomáštík
DIVINE je open-source nástroj pro ověřování LTL vlastností počítačových programů, který dokáže verifikovat mimo jiné i C/C++ kód. Přínos použití DIVINE je největší pro systémy využívající souběžnost; při volbě C/C++ jako vstupního jazyka to tedy znamená vícevláknové či víceprocesové programy. Cílem projektu je implementace modulu, který umožní pomocí DIVINE verifikovat programy používající MPI, široce rozšířený standard pro distribuované počítání.