Lista referatów

• 2009-12-07, godz. 10:15, 4790

  Artur Zawłocki (Uniwersytet Warszawski)

  Doktorat

  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)

  O weryfikacji bajtkodu Javy

  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)

  Prerun wystąpień w Eindhoven

• 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)

  Szkoła letnia ISS-AiPL

  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...

Strony