2011-03-14, godz. 10:15, 4790
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....
2011-03-07, godz. 10:15, 4790
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. ...
2011-02-28, godz. 10:15, 4790
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 seminariu...
2011-02-21, godz. 10:15, 4790
Aleksy Schubert (Uniwersytet Warszawski)
2011-02-14, godz. 10:15, 4790
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...
2011-01-17, godz. 10:15, 4790
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....
2011-01-10, godz. 10:15, 4790
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....
2010-12-20, godz. 10:15, 5850
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. ...
2010-12-13, godz. 10:15, 5850
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 ...
2010-12-06, godz. 10:15, 4790
Aleksy Schubert (Uniwersytet Warszawski)