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

  • 2010-03-15, godz. 10:15, 4790

    Patryk Czarnik (Uniwersytet Warszawski)

    A dozen instructions make Java bytecode

    Prerun przed Bytecode 2010.Abstrakt pracy:  One of the biggest obstacles in the formalisation of the Java  bytecode is that the language consists of 200 instructions.  However, a rigorous handling of a programming language in the  context of program verification and error detection requires a  ...

  • 2010-03-08, godz. 10:15, 4790

    Aleksy Schubert (Uniwersytet Warszawski)

    Mały bajtkod

    Aleksy opowie o wspólnej z Jackiem i Patrykiem pracy - sprowadzeniu całej funkcjonalności i wszystkich instrukcji Maszyny Wirtualnej Javy (JVM) do 12 instrukcji i zapisaniu operacyjnej semantyki małych kroków w postaci 23 reguł. Oczywiście instrukcje są sparametryzowane, aby móc reprezentow...

  • 2010-03-01, godz. 10:15, 4790

    Grzegorz Marczyński (Uniwersytet Warszawski)

    O granicach w kategorii praporządków z morfizmami słabo odbijającymi domknięcia w dół

    Podczas seminarium opowiem o moich zmaganiach z pokazaniem istnienia wszystkich granic w kategorii Preord!, której obiekty to praporządki, zaś morfizmy spełniają dwa warunki:(1) są monotoniczne(2) słabo odbijają domknięcia w dół, czyli dla f : A -> B, a\in A, b'\in B, jeśli b&#...

  • 2010-01-18, godz. 10:15, 4790

    Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)

    Prerun wystąpienia na SofSem 2010

    Będzie o automatycznym generowaniu anotacji, naszym narzędziu CodeStatistics i eksperymencie z pętlami for i decreases....

  • 2010-01-11, godz. 10:15, 4790

    Bartosz Zieliński (Wydział Fizyki i Informatyki Stosowanej, Uniwersytet Łódzki; Instytut Matematyki, PAN)

    Polityki i modele kontroli dostępu - kontynuacja

    Kontynuacja poprzedniego referatu, powtórka abstraktu: Omówione zostaną podstawowe pojęcia związane z bezpieczeństwem, modele kontroli dostępu, polityki bezpieczeństwa i związane z nimi problemy, m.in: rozróżnienie na uznaniową i obowiązkową kontrolę dostępu, podstawowy model macier...

  • 2010-01-04, godz. 10:15, 4790

    Bartosz Zieliński (Wydział Fizyki i Informatyki Stosowanej, Uniwersytet Łódzki; Instytut Matematyki, PAN)

    Polityki i modele kontroli dostępu

    Omówione zostaną podstawowe pojęcia związane z bezpieczeństwem, modele kontroli dostępu, polityki bezpieczeństwa i związane z nimi problemy, m.in: rozróżnienie na uznaniową i obowiązkową kontrolę dostępu, podstawowy model macierzy dostępu, model Harisona-Ruzzo-Ullmana i jego modyfika...

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

    Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)

    Analiza abstrakcyjna

    Na seminarium opowiemy o wykorzystaniu abstrakcyjnej interpretacji do analizy kodu programów. Skupimy się na zastosowaniu jej do sprawdzania występowania błędów rzepełnienia zakresu liczb całkowitych oraz wyjścia poza zakres tablicy w języku Java. W tym celu zaprezentujemy numeryczne abstr...

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

Strony