Organizatorzy

dr hab. Aleksy Schubert, prof. ucz.
prof. dr hab. Andrzej Tarlecki
prof. dr hab. Paweł Urzyczyn

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

12 kwietnia 2010 10:15
Michał R. Przybyłek (Uniwersytet Warszawski)
Kategoryjna teoria instytucji
Na seminarium opowiem o swoich najnowszych pracach związanych z kateogryjnym podejściem do połączenia, zmieniających się wzdłuż ustalonego języka, świata teorii i świata modeli. Będzie o modułach, prorozwłóknieniach i kategoryzacji pojęcia instytucji.
29 marca 2010 10:15
Tadeusz Sznuk (Uniwersytet Warszawski)
Generatory obligacji dowodowych
Zamierzam zacząc od powiedzenia, co to jest vcgen i jaką ma rolę w systemach weryfikacji. Potem omówię kilka takich systemów, w szczególności Vcc, Code contracts, KeY, Why, może też SPARK i Eiffel.
22 marca 2010 10:15
Maciej Zielenkiewicz (Uniwersytet Warszawski)
Teoria kategorii w Naturze
Na seminarium pokazane zostanie, jak w naturalny sposób teoria kategorii (i topologia) znajdują zastosowanie w kwantowej teorii pola, pozwalając zarówno na ułatwienie obliczeń, jak i na budowę "uogólnionych" teorii. Przedstawione zagadnienia zostaną zilustrowane analogiami do …
15 marca 2010 10:15
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 …
8 marca 2010 10:15
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 …
1 marca 2010 10:15
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 …
18 stycznia 2010 10:15
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.
11 stycznia 2010 10:15
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 macierzy dostępu, model …
4 stycznia 2010 10:15
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 modyfikacje, nierozstrzygalność …
14 grudnia 2009 10:15
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 …
7 grudnia 2009 10:15
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 …
30 listopada 2009 10:15
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ę …
16 listopada 2009 10:15
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łości. Do tego …
9 listopada 2009 10:15
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 …
2 listopada 2009 10:15
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 o własnych …