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

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 …
March 21, 2011, 10:15 a.m.
Tadeusz Sznuk (Uniwersytet Warszawski)
SAT solvery
SAT-solver, jaki jest, każdy widzi. Ale nie każdy przygląda się uważnie. Dlatego zamierzam opowiedzieć, co to dokładnie jest SAT-solver i jakie problemy można za pomocą takowego rozwiązywać Postaram się omówić dość szczegółowo architekturę CDCL, czyli …
March 14, 2011, 10:15 a.m.
Jędrzej Fulara (Uniwersytet Warszawski)
A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis
O pracy Cousot, Cousot, Logozzo z POPL2011 o takim tytule.
March 7, 2011, 10:15 a.m.
Maciej Zielenkiewicz (Uniwersytet Warszawski)
Generatory niezmienników i automatyczna weryfikacja II
Przedstawię sposób wykorzystania narzędzia ACSAR do automatycznej weryfikacji programów w Javie operujących na tablicach i znajdowania niezmienników pętli dla tych programów. Wystąpienie zilustrowane zostanie wynikami dla przykładowych programów.
Feb. 28, 2011, 10:15 a.m.
Krzysztof Jakubczyk (Uniwersytet Warszawski)
Zwiększanie dokładności dziedziny przedziałowej
Abstrakcyjna dziedzina przedziałów (ang. Intervals) jest bardzo szeroko wykorzystywaną dziedziną numeryczną. Niestety nie pozwala na dokładną reprezentację sumy dwóch elementów dziedziny (czyli m.in. zbiorów rozłącznych) co wpływa na zmniejszenie dokładności analizy. Na seminarium zaprezentuję sposoby …
Feb. 21, 2011, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Co będzie na ETAPSie
Feb. 14, 2011, 10:15 a.m.
Andrzej Tarlecki (Uniwersytet Warszawski)
Another old story: compositional property-oriented semantics for structured specifications
Abstract: Working in an arbitrary institution, we discuss property-orientedsemantics of specifications built using some collection ofspecification-building operations. As a typical example we consider thestructured specifications built from flat specifications using union,translation and hiding. For such …