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

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 …
Jan. 17, 2011, 10:15 a.m.
Jędrzej Fulara (Uniwersytet Warszawski)
Abstrakcyjne dziedziny do modelowania tablic
Przedstawię swoje prace nad dziedzinami do reprezentowania zawartości tablic. Zaprezentuję dwa rozwiązania: - wydajne, ale mało precyzyjne, oparte o dziedzinę przedziałową (wykorzystujące drzewa przedziałowe), - mniej wydajne, ale dokładniejsze, oparte o pentagony.
Jan. 10, 2011, 10:15 a.m.
Patryk Czarnik (Uniwersytet Warszawski)
Bajtkod Javy w 12 instrukcjach - założenia implementacji
Przypomnienie idei bajtkodu Javy w 12 instrukcjach oraz założenia co do implementacji jego semantyki w Coqu.
Dec. 20, 2010, 10:15 a.m.
Grzegorz Marczyński (Uniwersytet Warszawski)
Konstrukcje architekturalne w kategorii fragmentów
Na seminarium opowiem o kowariantnych sygnaturach i modelach konstrukcji architekturalnych oraz o ich składaniu. Pokażę też przykłady takich konstrukcji w kategorii fragmentów sygnatur algebraicznych z zależnościami.
Dec. 13, 2010, 10:15 a.m.
Andrzej Tarlecki (Uniwersytet Warszawski)
Perspectives Workshop: Formal Methods - Just a Euro-Science?
Opowiesci o spotkaniu w Schloss Daghstul, 1-3.12.2010. Przypominamy, że do końca grudnia seminarium odbywa się w ZMIENIONEJ SALI: 5850
Dec. 6, 2010, 10:15 a.m.
Aleksy Schubert (Uniwersytet Warszawski)
Oparte o dedukcję narzędzia sprawdzania poprawności kodu
Nov. 29, 2010, 10:15 a.m.
Maciej Zielenkiewicz (Uniwersytet Warszawski)
Generatory niezmienników i automatyczna weryfikacja
Przedstawię przegląd dostępnych gotowych programów umożliwiających automatyczną (z podaniem jedynie warunków początkowych i końcowych) weryfikację programów, ze szczególnym uwzględnieniem problemu odnajdywania niezmienników dla pętli. Jako przykład ciekawego i trudnego zagadnienia przedstawione zostaną programy operujące na …
Nov. 22, 2010, 10:15 a.m.
Krzysztof Jakubczyk (Uniwersytet Warszawski)
Dziedzina abstrakcyjna opisująca mnożenie zmiennych
Opowiem o pracy nad nową abstrakcyjną dziedziną numeryczną pozwalającą obsłużyć mnożenie zmiennych - będą to nierówności postaci xy <= c lub xy >=c, gdzie c może być liczbą ujemną lub dodatnią. Zaprezentuję bardziej szczegółowo podstawową …
Nov. 15, 2010, 10:15 a.m.
Jędrzej Fulara (Uniwersytet Warszawski)
Dziedzina abstrakcyjna 'Weighted Hexagons'
Opowiem o aktualnych pracach związanych z dziedziną abstrakcyjną 'Weighted Hexagons'.Pokażę jak rozszerzyć WH, aby obsługiwały również ostre nierówności. Opowiem o (dotychczas nieudanych) próbach zaadaptowania WH do przypadku całkowitoliczbowego (gdzie wartości zmiennych są liczbami całkowitymi).Powiem też …
Nov. 8, 2010, 10:15 a.m.
Tadeusz Sznuk (Uniwersytet Warszawski)
Co ja robię tu?
Opiszę projekt nowego BML-a. Na razie jest to tylko projekt projektu, więc nic konkretnego raczej nie powiem.