O weryfikacji bajtkodu Javy

Prelegent(ci)

Patryk Czarnik

Afiliacja

Uniwersytet Warszawski

Termin

2 listopada 2009 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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".

---