Nie jesteś zalogowany | Zaloguj się
Powrót do listy seminarów

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze.

Strona domowa: https://www.mimuw.edu.pl/~alx/piatek.html


Organizatorzy

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

  • 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 …

  • 17 stycznia 2011 10:15
    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.

  • 10 stycznia 2011 10:15
    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.

  • 20 grudnia 2010 10:15
    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.

  • 13 grudnia 2010 10:15
    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

  • 6 grudnia 2010 10:15
    Aleksy Schubert (Uniwersytet Warszawski)
    Oparte o dedukcję narzędzia sprawdzania poprawności kodu

  • 29 listopada 2010 10:15
    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 …

  • 22 listopada 2010 10:15
    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ą …

  • 15 listopada 2010 10:15
    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ż …