JVM w Coqu - odcinek i-ty

Speaker(s)

Patryk Czarnik

Affiliation

Uniwersytet Warszawski

Date

May 7, 2012, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---