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

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

Cotygodniowe seminarium badawcze


Organizatorzy

Informacje

piątki, 12:15 , sala: 5820

Dziedziny badań

Lista referatów

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

  • 12 kwietnia 2010 10:15
    Michał R. Przybyłek (Uniwersytet Warszawski)
    Kategoryjna teoria instytucji
    Na seminarium opowiem o swoich najnowszych pracach związanych z kateogryjnym podejściem do połączenia, zmieniających się wzdłuż ustalonego języka, świata teorii i świata modeli. Będzie o modułach, prorozwłóknieniach i kategoryzacji pojęcia instytucji.

  • 29 marca 2010 10:15
    Tadeusz Sznuk (Uniwersytet Warszawski)
    Generatory obligacji dowodowych
    Zamierzam zacząc od powiedzenia, co to jest vcgen i jaką ma rolę w systemach weryfikacji. Potem omówię kilka takich systemów, w szczególności Vcc, Code contracts, KeY, Why, może też SPARK i Eiffel.

  • 22 marca 2010 10:15
    Maciej Zielenkiewicz (Uniwersytet Warszawski)
    Teoria kategorii w Naturze
    Na seminarium pokazane zostanie, jak w naturalny sposób teoria kategorii (i topologia) znajdują zastosowanie w kwantowej teorii pola, pozwalając zarówno na ułatwienie obliczeń, jak i na budowę "uogólnionych" teorii. Przedstawione zagadnienia zostaną zilustrowane analogiami do …

  • 15 marca 2010 10:15
    Patryk Czarnik (Uniwersytet Warszawski)
    A dozen instructions make Java bytecode
    Prerun przed Bytecode 2010.Abstrakt pracy: One of the biggest obstacles in the formalisation of the Java bytecode is that the language consists of 200 instructions. However, a rigorous handling of a programming language in the …

  • 8 marca 2010 10:15
    Aleksy Schubert (Uniwersytet Warszawski)
    Mały bajtkod
    Aleksy opowie o wspólnej z Jackiem i Patrykiem pracy - sprowadzeniu całej funkcjonalności i wszystkich instrukcji Maszyny Wirtualnej Javy (JVM) do 12 instrukcji i zapisaniu operacyjnej semantyki małych kroków w postaci 23 reguł. Oczywiście instrukcje …

  • 1 marca 2010 10:15
    Grzegorz Marczyński (Uniwersytet Warszawski)
    O granicach w kategorii praporządków z morfizmami słabo odbijającymi domknięcia w dół
    Podczas seminarium opowiem o moich zmaganiach z pokazaniem istnienia wszystkich granic w kategorii Preord!, której obiekty to praporządki, zaś morfizmy spełniają dwa warunki:(1) są monotoniczne(2) słabo odbijają domknięcia w dół, czyli dla f : A …

  • 18 stycznia 2010 10:15
    Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)
    Prerun wystąpienia na SofSem 2010
    Będzie o automatycznym generowaniu anotacji, naszym narzędziu CodeStatistics i eksperymencie z pętlami for i decreases.

  • 11 stycznia 2010 10:15
    Bartosz Zieliński (Wydział Fizyki i Informatyki Stosowanej, Uniwersytet Łódzki; Instytut Matematyki, PAN)
    Polityki i modele kontroli dostępu - kontynuacja
    Kontynuacja poprzedniego referatu, powtórka abstraktu: Omówione zostaną podstawowe pojęcia związane z bezpieczeństwem, modele kontroli dostępu, polityki bezpieczeństwa i związane z nimi problemy, m.in: rozróżnienie na uznaniową i obowiązkową kontrolę dostępu, podstawowy model macierzy dostępu, model …

  • 4 stycznia 2010 10:15
    Bartosz Zieliński (Wydział Fizyki i Informatyki Stosowanej, Uniwersytet Łódzki; Instytut Matematyki, PAN)
    Polityki i modele kontroli dostępu
    Omówione zostaną podstawowe pojęcia związane z bezpieczeństwem, modele kontroli dostępu, polityki bezpieczeństwa i związane z nimi problemy, m.in: rozróżnienie na uznaniową i obowiązkową kontrolę dostępu, podstawowy model macierzy dostępu, model Harisona-Ruzzo-Ullmana i jego modyfikacje, nierozstrzygalność …

  • 14 grudnia 2009 10:15
    Jędrzej Fulara i Krzysztof Jakubczyk (Uniwersytet Warszawski)
    Analiza abstrakcyjna
    Na seminarium opowiemy o wykorzystaniu abstrakcyjnej interpretacji do analizy kodu programów. Skupimy się na zastosowaniu jej do sprawdzania występowania błędów rzepełnienia zakresu liczb całkowitych oraz wyjścia poza zakres tablicy w języku Java. W tym celu …

  • 7 grudnia 2009 10:15
    Artur Zawłocki (Uniwersytet Warszawski)
    Doktorat
    Opowiem o formalizmie, mojego autorstwa, do opisu systemów zbudowanych z komponentów, z których każdy porozumiewa się z otoczeniem za pośrednictwem akcji. Podobnie jak np. w CCS i CSP, komunikacja odbywa się przez synchronizację akcji: dwa …