Abstrakcyjne podejście do weryfikacji bajtkodu Javy

Weryfikacja bajtkodu to czynność przeprowadzana przez większość implementacji maszyny wirtualnej Javy podczas ładowania bajtkodu, w celu sprawdzenia poprawności programu przed jego uruchomieniem. W trakcie weryfikacji, w celu sprawdzenia poprawności typowej, przeprowadzana jest m.in. statyczna analiza przepływu danych. Bicolano to formalizacja maszyny wirtualnej oraz semantyki bajtkodu Javy opracowana w ramach projektu Mobius. Pracuję nad formalizacją algorytmu weryfikacji bajtkodu w Coqu, w oparciu o Bicolano. Moja formalizacja ma charakteryzować się tym, że algorytm nie rozpatruje bezpośrednio poszczególnych instrukcji, ale analizuje "sygnatury instrukcji" opisujące na poziomie typów jak instrukcja wpływa na stan. W połączeniu z modularną budową formalizacji, ma to ułatwić analizowanie weryfikacji bajtkodu dla różnych zestawów instrukcji i różnych hierarchii typów. Na seminarium przypomnę ogólniki, przypomnę pomysł sygnatur instrukcji oraz szczegółowo przedstawię formalizację "półkrat dobrze ufundowanych", czym zajmowałem się (razem z Jackiem) ostatnio. Przy okazji będzie coś o klasach w Coqu.