Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

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

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze

Plan referatów/Talks schedule

Lista referatów

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

  • 2010-11-08, godz. 10:15, 4790

    Tadeusz Sznuk (Uniwersytet Warszawski)

    Co ja robię tu?

    Opiszę projekt nowego BML-a. Na razie jest to tylko projekt projektu, więc nic konkretnego raczej nie powiem....

  • 2010-10-11, godz. 10:15, 4790

    Patryk Czarnik (Uniwersytet Warszawski)

    RiTS - środowisko do testowania klientów protokołów RCS

    RiTS to wewnętrzna nazwa jednego z projektów realizowanych w ramach współpracy UW z firmą Samsung. Głównym celem projektu jest zbudowanie systemu wspierającego testowanie klientów zestawu protokoów "Rich Communication Suite". Na najbliższym seminarium opowiem pobieżnie o protok...

  • 2010-10-04, godz. 10:15, 4790

    (Uniwersytet Warszawski)

    Ustalanie listy referatów

    Po wakacyjnej przerwie zapraszamy na seminarium SLIWOWICA.W poniedziałek 4 października przewidujemy spotkanie organizacyjne, na którym ustalimy wstępną listę referatów (lub co najmniej prelegentów) na semestr zimowy. Gorąco prosimy o zgłaszanie propozycji. Osoby, które nie będą mogły ...

  • 2010-05-17, godz. 10:15, 4790

    Patryk Czarnik (Uniwersytet Warszawski)

    RiTS - Rich Communication Suite Network Test Server

    Projekt RiTS jest realizowany w ramach współpracy Uniwersytetu Warzawskiego z firmą Samsung Electronics. Głównym celem projektu jest zbudowanie testowego serwera zestawu usług Rich Communication Suite. W ramach projektu poznajemy i analizujemy technologie i protokoły komunikacyjne, o które o...

  • 2010-05-10, godz. 10:15, 4790

    Andrzej Tarlecki (Uniwersytet Warszawski)

    SOME NUANCES OF MANY-SORTED UNIVERSAL ALGEBRA

    It has been a common belief that the standard results of universalalgebra as developed since the work of Birkhoff and others in thethirties carry over without much change to the framework ofmany-sorted algebras. Perhaps the only notable exception widelynoticed by the community is the care needed in ...

  • 2010-04-26, godz. 10:15, 4790

    Artur Zawłocki (Uniwersytet Warszawski)

    Prawdziwie współbieżna (truly-concurrent) semantyka dla wariantu CSP

    Na seminarium przedstawię (w zarysie) semantykę operacyjną idenotacyjną rachunku procesów, nad którym ostatnio pracuję. Rachunekprzypomina CSP Hoare'a, ma jednak kilka nietypowych cech:- Alfabety procesów podzielone są na akcje wejściowe i wyjściowe.- Semantyka uwzględnia obliczenia ...

  • 2010-04-19, godz. 10:15, 4790

    Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)

    Abstrakcyjna interpretacja nad dziedziną Weighted Hexagons

    Opowiemy jak zwykle o abstrakcyjnej interpretacji. Tym razem będziemy opisywać naszą abstrakcyjną dziedzinę numeryczną - Weighted Hexagons. Pozwala ona reprezentować: zależności postaci x <= a*y, gdzie x,y są zmiennymi oraz a jest stałą dodatnią, zależności przedziałowe czyli a ...

Strony