Organizatorzy

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

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

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
17 października 2011 10:15
Piotr Kosiuczenko (Wojskowa Akademia Techniczna)
Specyfikacja części nieimienniczej systemów w języku OCL
Specyfikacja kontraktowa pozwala opisać skutki wykonania metod. Ich wykonanie zwykle zmienia niewielki fragment systemu pozostawiając resztę bez zmian. Język JML posiada mechanizm służący do specyfikacji części niezmienniczej. OCL i niektóre inne języki kontraktowej specyfikacji takich …
10 października 2011 10:15
Tadeusz Sznuk (Uniwersytet Warszawski)
HAHA: Hoare Advanced Homework Assistant
Zamierzam opowiedzieć o koncepcji narzędzia, które ma służyć do wbijaniamłodym ludziom do głów podstaw logiki Hoare'a. Spróbuję pokazać podstawyEclipsowych technologii, których zamierzam użyć. Głównym celem jestzebranie uwag i pomysłów, w szczególności od osób, które przeżyłykontakt …
23 maja 2011 10:15
Andrzej Tarlecki (Uniwersytet Warszawski)
Interface Coherence of Reactive Software Components: Solutions and Challenges
Będzie to powtórzenie fragmentów referatu:Autor: Rolf Hennicker (Ludwig-Maximilians-Universität München)Opis: Interface coherence is a key issue in component-based softwaredevelopment. It concerns two dimensions of the development process:component implementations should adhere to their interface specifications- and - …
16 maja 2011 10:15
Michał R. Przybyłek (Uniwersytet Warszawski)
Uzupełnienia Dedekinda-MacNeilla
Dla dowolnego zbioru częściowo uporządkowanego P istnieje jego kowolne uzupełnienie \hat{P} do częściowego porządku posiadającego wszystkie kresy. \hat{P} można zdefiniować jako zbiór domkniętych w dół podzbiorów $P$ z naturalnie indukowanym porządkiem.Takie uzupełnienie zachowuje wszystkie istniejące …
16 maja 2011 10:15
Michał R. Przybyłek (Uniwersytet Warszawski)
Uzupełnienia Dedekinda-MacNeilla
Dla dowolnego zbioru częściowo uporządkowanego P istnieje jego kowolne uzupełnienie \hat{P} do częściowego porządku posiadającego wszystkie kresy. \hat{P} można zdefiniować jako zbiór domkniętych w dół podzbiorów $P$ z naturalnie indukowanym porządkiem.Takie uzupełnienie zachowuje wszystkie istniejące …
9 maja 2011 10:15
Aleksy Schubert (Uniwersytet Warszawski)
O testowaniu protokołów
11 kwietnia 2011 10:15
Jacek Chrząszcz (Uniwersytet Warszawski)
System do testowania klientów wielostronnych protokołów komunikacyjnych" czyli czym możemy się pochwalić po realizacji projektu RiTS
Referat będzie próbą wykrojenia publikowalnego materiału z projektuRiTS (RCS Network Test Server) zrealizowanego przez nas dla Samsunga.
4 kwietnia 2011 10:15
Tadeusz Sznuk (Uniwersytet Warszawski)
Diagramy decyzyjne i model checking CTL
Zapewne nie wszystkie z poniższych tematów zdążę poruszyć, ale ogólny plan wygląda tak: * Diagramy decyzyjne (BDD): - Definicje, struktura - Operacje - Uwagi implementacyjne - Warianty * Model checking: - Definicje: modele, formuły itp. …