Nie jesteś zalogowany | Zaloguj się
Facebook
LinkedIn
Powrót do listy aktywnych 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

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

  • 8 listopada 2010 10:15
    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.

  • 11 października 2010 10:15
    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 …

  • 4 października 2010 10:15
    - (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ą …

  • 17 maja 2010 10:15
    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, …

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

  • 26 kwietnia 2010 10:15
    Artur Zawłocki (Uniwersytet Warszawski)
    Prawdziwie współbieżna (truly-concurrent) semantyka dla wariantu CS)
    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 nieskończone …

  • 19 kwietnia 2010 10:15
    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 …