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

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. …
28 marca 2011 10:15
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 …
21 marca 2011 10:15
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 …
14 marca 2011 10:15
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.
7 marca 2011 10:15
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.
28 lutego 2011 10:15
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 …
21 lutego 2011 10:15
Aleksy Schubert (Uniwersytet Warszawski)
Co będzie na ETAPSie
14 lutego 2011 10:15
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 …