Informace o projektu
Informace o projektu
Verifikace MPI programů pomocí DIVINE
- Kód projektu
- MUNI/33/01/2015
- Období řešení
- 4/2015 - 12/2015
- Investor / Programový rámec / typ projektu
-
Masarykova univerzita
- Program děkana FI
- Fakulta / Pracoviště MU
-
Fakulta informatiky
- 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í.