Organizers

prof. dr hab. Paweł Urzyczyn

Information

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

Research fields

List of talks

March 7, 2011, 10:15 a.m.
Maciej Zielenkiewicz (Uniwersytet Warszawski)
Generatory niezmienników i automatyczna weryfikacja II
Przedstawię sposób wykorzystania narzędzia ACSAR do automatycznej weryfikacji programów w Javie operujących na tablicach i znajdowania niezmienników pętli dla tych programów. Wystąpienie zilustrowane zostanie wynikami dla przykładowych programów.
Feb. 28, 2011, 10:15 a.m.
Krzysztof Jakubczyk (Uniwersytet Warszawski)
Zwiększanie dokładności dziedziny przedziałowej
Abstrakcyjna dziedzina przedziałów (ang. Intervals) jest bardzo szeroko wykorzystywaną dziedziną numeryczną. Niestety nie pozwala na dokładną reprezentację sumy dwóch elementów dziedziny (czyli m.in. zbiorów rozłącznych) co wpływa na zmniejszenie dokładności analizy. Na seminarium zaprezentuję sposoby …
Feb. 21, 2011, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Co będzie na ETAPSie
Feb. 14, 2011, 10:15 a.m.
Andrzej Tarlecki (Uniwersytet Warszawski)
Another old story: compositional property-oriented semantics for structured specifications
Abstract: Working in an arbitrary institution, we discuss property-orientedsemantics of specifications built using some collection ofspecification-building operations. As a typical example we consider thestructured specifications built from flat specifications using union,translation and hiding. For such …
Jan. 17, 2011, 10:15 a.m.
Jędrzej Fulara (Uniwersytet Warszawski)
Abstrakcyjne dziedziny do modelowania tablic
Przedstawię swoje prace nad dziedzinami do reprezentowania zawartości tablic. Zaprezentuję dwa rozwiązania: - wydajne, ale mało precyzyjne, oparte o dziedzinę przedziałową (wykorzystujące drzewa przedziałowe), - mniej wydajne, ale dokładniejsze, oparte o pentagony.
Jan. 10, 2011, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
Bajtkod Javy w 12 instrukcjach - założenia implementacji
Przypomnienie idei bajtkodu Javy w 12 instrukcjach oraz założenia co do implementacji jego semantyki w Coqu.
Dec. 20, 2010, 10:15 a.m.
Grzegorz Marczyński (Uniwersytet Warszawski)
Konstrukcje architekturalne w kategorii fragmentów
Na seminarium opowiem o kowariantnych sygnaturach i modelach konstrukcji architekturalnych oraz o ich składaniu. Pokażę też przykłady takich konstrukcji w kategorii fragmentów sygnatur algebraicznych z zależnościami.
Dec. 13, 2010, 10:15 a.m.
Andrzej Tarlecki (Uniwersytet Warszawski)
Perspectives Workshop: Formal Methods - Just a Euro-Science?
Opowiesci o spotkaniu w Schloss Daghstul, 1-3.12.2010. Przypominamy, że do końca grudnia seminarium odbywa się w ZMIENIONEJ SALI: 5850
Dec. 6, 2010, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Oparte o dedukcję narzędzia sprawdzania poprawności kodu
Nov. 29, 2010, 10:15 a.m.
Maciej Zielenkiewicz (Uniwersytet Warszawski)
Generatory niezmienników i automatyczna weryfikacja
Przedstawię przegląd dostępnych gotowych programów umożliwiających automatyczną (z podaniem jedynie warunków początkowych i końcowych) weryfikację programów, ze szczególnym uwzględnieniem problemu odnajdywania niezmienników dla pętli. Jako przykład ciekawego i trudnego zagadnienia przedstawione zostaną programy operujące na …
Nov. 22, 2010, 10:15 a.m.
Krzysztof Jakubczyk (Uniwersytet Warszawski)
Dziedzina abstrakcyjna opisująca mnożenie zmiennych
Opowiem o pracy nad nową abstrakcyjną dziedziną numeryczną pozwalającą obsłużyć mnożenie zmiennych - będą to nierówności postaci xy <= c lub xy >=c, gdzie c może być liczbą ujemną lub dodatnią. Zaprezentuję bardziej szczegółowo podstawową …
Nov. 15, 2010, 10:15 a.m.
Jędrzej Fulara (Uniwersytet Warszawski)
Dziedzina abstrakcyjna 'Weighted Hexagons'
Opowiem o aktualnych pracach związanych z dziedziną abstrakcyjną 'Weighted Hexagons'.Pokażę jak rozszerzyć WH, aby obsługiwały również ostre nierówności. Opowiem o (dotychczas nieudanych) próbach zaadaptowania WH do przypadku całkowitoliczbowego (gdzie wartości zmiennych są liczbami całkowitymi).Powiem też …
Nov. 8, 2010, 10:15 a.m.
Tadeusz Sznuk (Uniwersytet Warszawski)
Co ja robię tu?
Opiszę projekt nowego BML-a. Na razie jest to tylko projekt projektu, więc nic konkretnego raczej nie powiem.
Oct. 11, 2010, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
RiTS - środowisko do testowania klientów protokołów RCS
RiTS to wewnętrzna nazwa jednego z projektów realizowanych w ramach współpracy UW z firmą Samsung. Głównym celem projektu jest zbudowanie systemu wspierającego testowanie klientów zestawu protokoów "Rich Communication Suite". Na najbliższym seminarium opowiem pobieżnie o …
Oct. 4, 2010, 10:15 a.m.
- (Uniwersytet Warszawski)
Ustalanie listy referatów
Po wakacyjnej przerwie zapraszamy na seminarium SLIWOWICA.W poniedziałek 4 października przewidujemy spotkanie organizacyjne, na którym ustalimy wstępną listę referatów (lub co najmniej prelegentów) na semestr zimowy. Gorąco prosimy o zgłaszanie propozycji. Osoby, które nie będą …