Lista referatów

• 2012-03-19, godz. 10:15, 4790

  Tadeusz Sznuk (Uniwersytet Warszawski)

  HAHA

  Zamierzam powiedzieć mniej więcej to samo, co poprzednio, czyli do czego to narzędzie ma służyć i jak ma działać. Z tą różnicą, że zamiast slajdów będę się posługiwał prototypem implementacji....

• 2012-03-12, godz. 10:15, 4790

  Aleksy Schubert (Uniwersytet Warszawski)

  Czytelne programowanie

  ...

• 2012-02-20, godz. 10:15, 4790

  Michał Roman Przybyłek (Uniwersytet Warszawski)

  Wariacje na Systemach Logicznych

  ...

• 2012-01-16, godz. 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, godz. 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, godz. 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, godz. 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, godz. 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, godz. 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, godz. 10:15, 4790

  Andrzej Tarlecki (Uniwersytet Warszawski)

  O semantyce specyfikacji structuralnych zorientowanej na własności

Strony