Automatyczna weryfikacja działających w sieci (np. w Internecie) systemów rozproszonych o skończonej lub nieskończonej liczbie stanów, wykonywana poprzez analizę ich przestrzeni stanów, jest niezwykle aktywną dziedziną badawczą, która już od kilkunastu lat przynosi obiecujące praktyczne rozwiązania. W ramach poprzedniego projektu KBN Automatyczna weryfikacja systemów zależnych od czasu nasz zespół opracował, zaimplementował i uruchomił system weryfikacyjny VerICS. Opis systemu został opublikowany na dwóch renomowanych konferencjach w tej dziedzinie: zagranicznej TACAS'03 [DJJ+03a] i polskiej SCR'03 [DJJ+03b], a sam system jest dostępny poprzez interfejs www pod adresem http://pegaz.ipipan.waw.pl/~verics/. Ponadto wyniki projektu, opublikowane w ponad 30 pracach, zostały bardzo wysoko ocenione przez KBN, co znalazło wyraz w ocenie końcowej projektu "znakomity". Projekt ten miał charakter zdecydowanie teoretyczny (opracowanie nowych metod weryfikacji i ich matematyczne uzasadnienie). Obecny projekt zamierzamy zorientować na cele praktyczne. Jego głównym zamierzeniem jest opracowanie środowiska programistycznego ułatwiającego zewnętrzny dostęp do systemu VerICS i zastosowanie go do weryfikacji poprawności rozproszonych systemów oprogramowania i protokołów kryptograficznych.