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

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ą …
May 17, 2010, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
RiTS - Rich Communication Suite Network Test Server
Projekt RiTS jest realizowany w ramach współpracy Uniwersytetu Warzawskiego z firmą Samsung Electronics. Głównym celem projektu jest zbudowanie testowego serwera zestawu usług Rich Communication Suite. W ramach projektu poznajemy i analizujemy technologie i protokoły komunikacyjne, …
May 10, 2010, 10:15 a.m.
Andrzej Tarlecki (Uniwersytet Warszawski)
SOME NUANCES OF MANY-SORTED UNIVERSAL ALGEBRA
It has been a common belief that the standard results of universalalgebra as developed since the work of Birkhoff and others in thethirties carry over without much change to the framework ofmany-sorted algebras. Perhaps the …
April 26, 2010, 10:15 a.m.
Artur Zawłocki (Uniwersytet Warszawski)
truly-concurrent) semantyka dla wariantu CS (Prawdziwie współbieżna)
Na seminarium przedstawię (w zarysie) semantykę operacyjną idenotacyjną rachunku procesów, nad którym ostatnio pracuję. Rachunekprzypomina CSP Hoare'a, ma jednak kilka nietypowych cech:- Alfabety procesów podzielone są na akcje wejściowe i wyjściowe.- Semantyka uwzględnia obliczenia nieskończone …
April 19, 2010, 10:15 a.m.
Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)
Abstrakcyjna interpretacja nad dziedziną Weighted Hexagons
Opowiemy jak zwykle o abstrakcyjnej interpretacji. Tym razem będziemy opisywać naszą abstrakcyjną dziedzinę numeryczną - Weighted Hexagons. Pozwala ona reprezentować: zależności postaci x <= a*y, gdzie x,y są zmiennymi oraz a jest stałą dodatnią, zależności …