Organizers

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

Information

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

Research fields

List of talks

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
Oct. 17, 2011, 10:15 a.m.
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 …
Oct. 10, 2011, 10:15 a.m.
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 …
May 23, 2011, 10:15 a.m.
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 - …
May 16, 2011, 10:15 a.m.
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 …
May 16, 2011, 10:15 a.m.
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 …
May 9, 2011, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
O testowaniu protokołów
April 11, 2011, 10:15 a.m.
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.
April 4, 2011, 10:15 a.m.
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. …
March 28, 2011, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
JVM w Coqu - struktury czasu wykonania
Staram się zaimplementować w Coqu semantykę bajtkodu Javy w wersji wykorzystującej "faktoryzację" i "parametryzację" (bajtkod w 12 instrukcji).Na seminarium przedstawię definicje typów dla struktur czasu wykonania. Mam nadzieję na dyskusję i rady co do sensowności …