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)
2010-11-29, godz. 10:15, 4790
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 zagadnieni...
2010-11-22, godz. 10:15, 4790
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ą wersję dziedziny oraz opowie...
2010-11-15, godz. 10:15, 4790
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ą l...