Mały bajtkod

Prelegent(ci)

Aleksy Schubert

Afiliacja

Uniwersytet Warszawski

Termin

8 marca 2010 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Aleksy opowie o wspólnej z Jackiem i Patrykiem pracy - sprowadzeniu całej funkcjonalności i wszystkich instrukcji Maszyny Wirtualnej Javy (JVM) do 12 instrukcji i zapisaniu operacyjnej semantyki małych kroków w postaci 23 reguł. Oczywiście instrukcje są sparametryzowane, aby móc reprezentować wszystkie instrukcje oryginalnego języka, a wybór 12 instrukcji jest oparty o sposób korzystania ze struktur danych JVM.

Staraliśmy się pokryć cały język JVML i co najmniej umożliwić uwzględnienie wszystkich aspektów, takich jak współbieżność czy Java Memory Model. Na seminarium przedstawione zostaną też pomysły na dalsze rozwinięcie tego tematu w kierunku formalizcji tej pracy w Coqu, wykorzystania do analiz statycznych/abstrakcyjnych interpretacji, czy opracowania analogicznie "skompresowanego" języka specyfikacji dla JVM.

---