2009-12-07, godz. 10:15, 4790
Artur Zawłocki (Uniwersytet Warszawski)
Opowiem o formalizmie, mojego autorstwa, do opisu systemów zbudowanych z komponentów, z których każdy porozumiewa siÄ™ z otoczeniem za poÅ›rednictwem akcji. Podobnie jak np. w CCS i CSP, komunikacja odbywa siÄ™ przez synchronizacjÄ™ akcji: dwa komponenty można połączyć przez sparowanie 'wyjÅ...
2009-11-30, godz. 10:15, 4790
Piotr Kosiuczenko
Efektywna implementacja operatora @pre/old i jej weryfikacja
Referat dotyczy implementacji operatorów zwracających wartość parametru sprzed wykonania operacji takich jak @pre w języku OCL oraz \old w językach JML i Spec#. Dotychczasowe implementacje nie gwarantowały żadnych ograniczeń czasowych, a nawet własności zatrzymywania się programu. Z drug...
2009-11-16, godz. 10:15, 4790
Grzegorz Marczyński (Uniwersytet Warszawski)
Sygnatury algebraiczne z porzÄ…dkiem na symbolach
Na seminarium przedstawię wyniki mojej pracy nad sygnaturami algebraicznymi, które zawierają relację zależności pomiędzy symbolami. Pokażę też definicję kategorii fragmentów takich sygnatur, pullback-pushout uzupełnień, oraz kilku funktorów służących do "domykania" fragmentów w ca...
2009-11-09, godz. 10:15, 4790
Aleksy Schubert (Uniwersytet Warszawski)
Co się działo na drugim światowym kongresie Formal Methods
Duże konferencje wyznaczają zwykle trendy w badaniach nad danym tematem. Zwłaszcza dotyczy to zaproszonych wykładów. Na referacie zaprezentuję streszczenie zaproszonych wykładów: + Formal Methods for Privacy, Jeanette Wing + What can Formal Methods bring do Systems Biology?, Wan Fokkink +...
2009-11-02, godz. 10:15, 4790
Patryk Czarnik (Uniwersytet Warszawski)
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 ...
2009-10-26, godz. 10:15, 4790
Aleksy Schubert (Uniwersytet Warszawski)
2009-10-19, godz. 10:15, 4790
Aleksy Schubert i Jacek ChrzÄ…szcz (Uniwersytet Warszawski)
Weryfikacja skompilowanych klas Javy w oparciu o specyfikacjÄ™ w BML - studium przypadku
W ramach zakończonego niedawno projektu Mobius powstało szereg narzędzi do specyfikacji i weryfikacji własności programów w Javie. Jednym z narzędzi jest generator obligacji dowodowych BMLVCGen, który na podstawie pliku ze skompilowaną klasą Javy wzbogaconą o binarne specyfikacje w język...
2009-10-12, godz. 10:15, 4790
Patryk Czarnik (Uniwersytet Warszawski)
W sierpniu miałem przyjemność w Edynburgu brać udział w szkole International Summer School on Advances in Programming Languages http://www.macs.hw.ac.uk/~greg/ISS-AiPL/ Na seminarium postaram się streścić 10 wykładów Szkoły :), a tak naprawdę zapewne uda się nieco dokładniej omówić...
2009-10-05, godz. 10:15, 4790
(Uniwersytet Warszawski)
Spotkanie organizacyjne, ustalanie tematów referatów.
...
2009-05-04, godz. 10:15, 4790
Patryk Czarnik (Uniwersytet Warszawski)
Abstrakcyjne podejście do weryfikacji bajtkodu Javy
Weryfikacja bajtkodu to czynność przeprowadzana przez większość implementacji maszyny wirtualnej Javy podczas ładowania bajtkodu, w celu sprawdzenia poprawności programu przed jego uruchomieniem. W trakcie weryfikacji, w celu sprawdzenia poprawności typowej, przeprowadzana jest m.in. statycz...