Mały bajtkod

Speaker(s)

Aleksy Schubert

Affiliation

Uniwersytet Warszawski

Date

March 8, 2010, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---