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

  • 2012-01-16, 10:15, 4790

    Bartek Klin (Uniwersytet Warszawski)

    Prerun wykładów habilitacyjnych

    TEMAT 1:  Mądrej głowie dość dwie słowie, czyli dowody probabilistycznie sprawdzalneJak sprawdzić, czy dowód twierdzenia matematycznego jest poprawny, nie czytając go w całości? Dla pewnej klasy problemów i dowodów jest to możliwe. Dowód probabilistycznie sprawdzalny to taki, który m...

  • 2012-01-09, 10:15, 4790

    Patryk Czarnik (Uniwersytet Warszawski)

    JVM w Coqu po mojemu czyli faktoryzacja faktoryzacji

    Chodzi oczywiście o formalizację w Coqu semantyki maszyny wirtualnej Javy. Ogólnie będzie... jak zwykle, a w szczegółach - jak realizuję operacje na stosie wartości (tzw. stackop) i jakie wnioski z tego wynikają dla całej formalizacji....

  • 2011-12-19, 10:15, 4790

    Jerzy Tyszkiewicz (Uniwersytet Warszawski)

    Parallel Random Access Machines and Spreadsheets Are (Almost) the Same

    W referacie (po polsku, tytuł i slajdy po angielsku) pokażę, że w arkuszach kalkulacyjnych można nie używając żadnych makr zaimplementować interpreter maszyny PRAM (Parallel Random Access Machine). Wskazuje to zarazem na: 1) Możliwość wyrażania w arkuszach bardzo skomplikowanych oblicze...

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

    Bartek Klin (Uniwersytet Warszawski)

    Logiczne prawa rozdzielności

    Opowiem o metodzie dowodzenia kompozycjonalnościrównoważności behawioralnych za pomocą układów równań międzyoperatorami modalnymi. Najpierw przypomnę, co to są koalgebry,bialgebry, logiki modalne i SOS....

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

    Tadeusz Sznuk (Uniwersytet Warszawski)

    Fluid Updates in Arbitrary Abstract Domains

    "Fluid updates" (płynne aktualizacje?) to mechanizm stosowany przy analizie programów operujących na tablicach, przedstawiony w pracy [DDA10]. Wykorzystuje on formuły logiki pierwszego rzędu, których spełnialność weryfikowana jest przez SMT-solver. Podczas prezentacji pokażę, jak uogólni...

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

    Krzysztof Jakubczyk (Uniwersytet Warszawski)

    Sweeping in Abstract Interpretation

    Tym razem opowiem o swojej pracy którą prezentowałem na workshopie NSAD 2011 - "Sweeping in Abstract Interpretation", swoich wrażeniach oraz innych pracach które były tam prezentowane....

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

    Andrzej Tarlecki (Uniwersytet Warszawski)

    O semantyce specyfikacji structuralnych zorientowanej na własności

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

    Piotr Kosiuczenko (Wojskowa Akademia Techniczna)

    Specyfikacja części nieimienniczej systemów w języku OCL

    Specyfikacja kontraktowa pozwala opisać  skutki wykonania metod. Ich wykonanie zwykle zmienia niewielki fragment systemu pozostawiając resztę bez zmian. Język JML posiada mechanizm służący do specyfikacji części niezmienniczej. OCL i niektóre inne języki kontraktowej specyfikacji takich ...

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

    Tadeusz Sznuk (Uniwersytet Warszawski)

    HAHA: Hoare Advanced Homework Assistant

    Zamierzam opowiedzieć o koncepcji narzędzia, które ma służyć do wbijaniamłodym ludziom do głów podstaw logiki Hoare'a. Spróbuję pokazać podstawyEclipsowych technologii, których zamierzam użyć. Głównym celem jestzebranie uwag i pomysłów, w szczególności od osób, które prze...

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

    Andrzej Tarlecki (Uniwersytet Warszawski)

    Interface Coherence of Reactive Software Components: Solutions and Challenges

    Będzie to powtórzenie fragmentów referatu:Autor: Rolf Hennicker (Ludwig-Maximilians-Universität München)Opis: Interface coherence is a key issue in component-based softwaredevelopment. It concerns two dimensions of the development process:component implementations should adhere to their interfa...

Pages