Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze

Plan referatów/Talks schedule

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