You are not logged in | Log in
Return to the list of active seminars

Seminar Semantics, Logic, Verification and its Applications

Weekly research seminar

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


Organizers

Information

Fridays, 12:15 p.m. , room: 5450

Research fields

List of talks

  • April 11, 2011, 10:15 a.m.
    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.

  • April 4, 2011, 10:15 a.m.
    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. …

  • March 28, 2011, 10:15 a.m.
    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 …

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