Informace o projektu
Verifikace MPI programů pomocí DIVINE
| Kód projektu | MUNI/33/01/2015 CEP CORDIS MU WEB INET MU |
|---|---|
| Doba řešení | 01.04.2015–31.12.2015 |
| Stav | ukončený |
| Investor | Masarykova univerzita |
| Program | Program děkana FI |
| Řešitel za FI |
Anotace
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í.