O weryfikacji bajtkodu Javy

Speaker(s)

Patryk Czarnik

Affiliation

Uniwersytet Warszawski

Date

Nov. 2, 2009, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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

---