O weryfikacji bajtkodu Javy

Weryfikacja bajtkodu to operacja wykonywana przez większość impementacji Maszyny Wirtualnej Javy podczas ładowania klas, której celem jest sprawdzenie poprawności bajtkodu, ze szczególnym uwzględnieniem zgodności typów argumentów dla poszczególnych instruckji JVM. Na seminarium opowiem o własnych (we współpracy z Jackiem Chrząszczem i Aleksym Schubertem) próbach formalizacji weryfikacji bajtkodu w Coqu, w oparciu o Mobiusową formalizację JVM "Bicolano".