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

28 maja 2012 10:15
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 …
14 maja 2012 10:15
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.
7 maja 2012 10:15
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] …
16 kwietnia 2012 10:15
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 …
26 marca 2012 10:15
Artur Zawłocki (Uniwersytet Warszawski)
Specyfikacja systemów komponentowych (badania własne)
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 …
19 marca 2012 10:15
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.
12 marca 2012 10:15
Aleksy Schubert (Uniwersytet Warszawski)
Czytelne programowanie
20 lutego 2012 10:15
Michał Roman Przybyłek (Uniwersytet Warszawski)
Wariacje na Systemach Logicznych
16 stycznia 2012 10:15
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 …
9 stycznia 2012 10:15
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.
19 grudnia 2011 10:15
Jerzy Tyszkiewicz (Uniwersytet Warszawski)
Parallel Random Access Machines and Spreadsheets Are (Almost) the Sam)
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 …
5 grudnia 2011 10:15
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.
28 listopada 2011 10:15
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 …
7 listopada 2011 10:15
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.
24 października 2011 10:15
Andrzej Tarlecki (Uniwersytet Warszawski)
O semantyce specyfikacji structuralnych zorientowanej na własności