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

May 28, 2012, 10:15 a.m.
Jędrzej Fulara (Uniwersytet Warszawski)
Analiza abstrakcyjna zmiennych numerycznych oraz kontenerów danych
Tym razem nie opowiem o niczym, czego byście jeszcze nie słyszeli. Referat będzie o abstrakcyjnej interpretacji oraz dziedzinach numerycznych i dziedzinach do analizy zawartości kontenerów danych, takich jak tablice i słowniki. Pojawią się (bez technicznych …
May 14, 2012, 10:15 a.m.
Michał Roman Przybyłek (Uniwersytet Warszawski)
Moduły nad monadami
Opowiem o formalnej teorii monad w bikategoriach. W szczególności skupię się na charakteryzacji rezolucji monad za pomocą uniwersalnych modułów i luźnych (ko)stożków.
May 7, 2012, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
JVM w Coqu - odcinek i-ty
Referat o tym, co zwykle, czyli o moich przygodach z formalizacją bajtkodu Javy Coq-u.W najbliższym odcinku:* "właściwie to mam prawie wszystkie instrukcje operujące wewnątrz ramki" ;),* dowód własności programu z pętlą (suma 2*i-1 dla i:[1..n] …
April 16, 2012, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
Testing of Evolving Protocols
Prerun przed workshopem "Testing: Academic & Industrial Conference Practice and Research Techniques" (http://www2012.taicpart.org)Abstrakt pracy (wspólnej z J. Chrząszczem, A. Schubertem i A. Tarleckim): A common assumption for the state-of-the-art methods of protocol testing is that …
March 26, 2012, 10:15 a.m.
Artur Zawłocki (Uniwersytet Warszawski)
badania własne (Specyfikacja systemów komponentowych)
Przedstawię podejście do specyfikacji systemów złożonych zewspółbieżnych, komunikujących się synchronicznie komponentów, które umożliwia kompozycjonalną specyfikację i weryfikację (o własnościach systemu można wnioskować na podstawie własności komponentów) oraz wspiera refinement specyfikacji (przechodzenie od specyfikacji abstrakcyjnej do …
March 19, 2012, 10:15 a.m.
Tadeusz Sznuk (Uniwersytet Warszawski)
HAHA
Zamierzam powiedzieć mniej więcej to samo, co poprzednio, czyli do czego to narzędzie ma służyć i jak ma działać. Z tą różnicą, że zamiast slajdów będę się posługiwał prototypem implementacji.
March 12, 2012, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Czytelne programowanie
Feb. 20, 2012, 10:15 a.m.
Michał Roman Przybyłek (Uniwersytet Warszawski)
Wariacje na Systemach Logicznych
Jan. 16, 2012, 10:15 a.m.
Bartek Klin (Uniwersytet Warszawski)
Prerun wykładów habilitacyjnych
TEMAT 1: Mądrej głowie dość dwie słowie, czyli dowody probabilistycznie sprawdzalneJak sprawdzić, czy dowód twierdzenia matematycznego jest poprawny, nie czytając go w całości? Dla pewnej klasy problemów i dowodów jest to możliwe. Dowód probabilistycznie sprawdzalny …
Jan. 9, 2012, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
JVM w Coqu po mojemu czyli faktoryzacja faktoryzacji
Chodzi oczywiście o formalizację w Coqu semantyki maszyny wirtualnej Javy. Ogólnie będzie... jak zwykle, a w szczegółach - jak realizuję operacje na stosie wartości (tzw. stackop) i jakie wnioski z tego wynikają dla całej formalizacji.
Dec. 19, 2011, 10:15 a.m.
Jerzy Tyszkiewicz (Uniwersytet Warszawski)
Almost) the Sam (Parallel Random Access Machines and Spreadsheets Are)
W referacie (po polsku, tytuł i slajdy po angielsku) pokażę, że w arkuszach kalkulacyjnych można nie używając żadnych makr zaimplementować interpreter maszyny PRAM (Parallel Random Access Machine). Wskazuje to zarazem na: 1) Możliwość wyrażania w …
Dec. 5, 2011, 10:15 a.m.
Bartek Klin (Uniwersytet Warszawski)
Logiczne prawa rozdzielności
Opowiem o metodzie dowodzenia kompozycjonalnościrównoważności behawioralnych za pomocą układów równań międzyoperatorami modalnymi. Najpierw przypomnę, co to są koalgebry,bialgebry, logiki modalne i SOS.
Nov. 28, 2011, 10:15 a.m.
Tadeusz Sznuk (Uniwersytet Warszawski)
Fluid Updates in Arbitrary Abstract Domains
"Fluid updates" (płynne aktualizacje?) to mechanizm stosowany przy analizie programów operujących na tablicach, przedstawiony w pracy [DDA10]. Wykorzystuje on formuły logiki pierwszego rzędu, których spełnialność weryfikowana jest przez SMT-solver. Podczas prezentacji pokażę, jak uogólnić ów …
Nov. 7, 2011, 10:15 a.m.
Krzysztof Jakubczyk (Uniwersytet Warszawski)
Sweeping in Abstract Interpretation
Tym razem opowiem o swojej pracy którą prezentowałem na workshopie NSAD 2011 - "Sweeping in Abstract Interpretation", swoich wrażeniach oraz innych pracach które były tam prezentowane.
Oct. 24, 2011, 10:15 a.m.
Andrzej Tarlecki (Uniwersytet Warszawski)
O semantyce specyfikacji structuralnych zorientowanej na własności