JVM w Coqu - odcinek i-ty

Prelegent(ci)

Patryk Czarnik

Afiliacja

Uniwersytet Warszawski

Termin

7 maja 2012 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Referat o tym, co zwykle, czyli o moich przygodach z formalizacją bajtkodu Javy Coq-u.
W najbliższym odcinku:
* "właściwie to mam prawie wszystkie instrukcje  operujące wewnątrz ramki" ;),
* dowód własności programu z pętlą (suma 2*i-1 dla i:[1..n] = n*n),
* machanie rękami na temat uogólnienia techniki tego dowodu i zrobienia czegoś na kształt logiki Hoare'a dla bajtkodu,
* błędy w (mojej) specyfikacji znalezione w trakcie testowego dowodu oraz refaktoryzacja faktoryzacji.

---