Nie jesteś zalogowany |
Cotygodniowe seminarium badawcze
Lista referató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 …
-
-
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.
