You are not logged in | log in

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Seminar Semantics, Logic, Verification and its Applications

Weekly research seminar


List of talks

  • 2011-05-16, 10:15, 4790

    Michał R. Przybyłek (Uniwersytet Warszawski)

    Uzupełnienia Dedekinda-MacNeilla

    Dla dowolnego zbioru częściowo uporządkowanego P istnieje jego kowolne uzupełnienie \hat{P} do częściowego porządku posiadającego wszystkie kresy. \hat{P} można zdefiniować jako zbiór domkniętych w dół podzbiorów $P$ z naturalnie indukowanym porządkiem.Takie uzupełnienie zachowuje w...

  • 2011-05-16, 10:15, 4790

    Michał R. Przybyłek (Uniwersytet Warszawski)

    Uzupełnienia Dedekinda-MacNeilla

    Dla dowolnego zbioru częściowo uporządkowanego P istnieje jego kowolne uzupełnienie \hat{P} do częściowego porządku posiadającego wszystkie kresy. \hat{P} można zdefiniować jako zbiór domkniętych w dół podzbiorów $P$ z naturalnie indukowanym porządkiem.Takie uzupełnienie zachowuje w...

  • 2011-05-09, 10:15, 4790

    Aleksy Schubert (Uniwersytet Warszawski)

    O testowaniu protokołów

  • 2011-04-11, 10:15, 4790

    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....

  • 2011-04-04, 10:15, 4790

    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...

  • 2011-03-28, 10:15, 4790

    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 owij...

  • 2011-03-21, 10:15, 4790

    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 najpopularniejszy ostat...

  • 2011-03-14, 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, 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, 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...

Pages