Organizers

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

Information

Fridays, 12:15 p.m. , room: 5450

Research fields

List of talks

April 12, 2010, 10:15 a.m.
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.
March 29, 2010, 10:15 a.m.
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.
March 22, 2010, 10:15 a.m.
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 …
March 15, 2010, 10:15 a.m.
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 …
March 8, 2010, 10:15 a.m.
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 …
March 1, 2010, 10:15 a.m.
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 …
Jan. 18, 2010, 10:15 a.m.
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.
Jan. 11, 2010, 10:15 a.m.
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 …
Jan. 4, 2010, 10:15 a.m.
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ść …
Dec. 14, 2009, 10:15 a.m.
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 …
Dec. 7, 2009, 10:15 a.m.
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 …
Nov. 30, 2009, 10:15 a.m.
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ę …
Nov. 16, 2009, 10:15 a.m.
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 …
Nov. 9, 2009, 10:15 a.m.
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 …
Nov. 2, 2009, 10:15 a.m.
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 …