Lista referatów

• 2011-10-17, godz. 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, godz. 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, godz. 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...

• 2011-05-16, godz. 10:15, 4790

  Michał R. Przybyłek (Uniwersytet Warszawski)

  Uzupełnienia Dedekinda-MacNeilla

  Dla dowolnego zbioru częściowo uporządkowanego P istnieje jego kowolne uzupełnienie \hat{P} do częściowego porządku posiadającego wszystkie kresy. \hat{P} można zdefiniować jako zbiór domkniętych w dół podzbiorów $P$ z naturalnie indukowanym porządkiem.Takie uzupełnienie zachowuje w...

• 2011-05-16, godz. 10:15, 4790

  Michał R. Przybyłek (Uniwersytet Warszawski)

  Uzupełnienia Dedekinda-MacNeilla

  Dla dowolnego zbioru częściowo uporządkowanego P istnieje jego kowolne uzupełnienie \hat{P} do częściowego porządku posiadającego wszystkie kresy. \hat{P} można zdefiniować jako zbiór domkniętych w dół podzbiorów $P$ z naturalnie indukowanym porządkiem.Takie uzupełnienie zachowuje w...

• 2011-05-09, godz. 10:15, 4790

  Aleksy Schubert (Uniwersytet Warszawski)

  O testowaniu protokołów

• 2011-04-11, godz. 10:15, 4790

  Jacek ChrzÄ…szcz (Uniwersytet Warszawski)

  System do testowania klientów wielostronnych protokołów komunikacyjnych" czyli czym możemy się pochwalić po realizacji projektu RiTS

  Referat będzie próbą wykrojenia publikowalnego materiału z projektuRiTS (RCS Network Test Server) zrealizowanego przez nas dla Samsunga....

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

  Tadeusz Sznuk (Uniwersytet Warszawski)

  Diagramy decyzyjne i model checking CTL

  Zapewne nie wszystkie z poniższych tematów zdążę poruszyć, ale ogólny plan wyglÄ…da tak:   * Diagramy decyzyjne (BDD):       - Definicje, struktura       - Operacje       - Uwagi implementacyjne       - Warianty   * Model checking:       - Definicje: modele, formuÅ...

• 2011-03-28, godz. 10:15, 4790

  Patryk Czarnik (Uniwersytet Warszawski)

  JVM w Coqu - struktury czasu wykonania

  Staram się zaimplementować w Coqu semantykę bajtkodu Javy w wersji wykorzystującej "faktoryzację" i "parametryzację" (bajtkod w 12 instrukcji).Na seminarium przedstawię definicje typów dla struktur czasu wykonania. Mam nadzieję na dyskusję i rady co do sensowności owij...

• 2011-03-21, godz. 10:15, 4790

  Tadeusz Sznuk (Uniwersytet Warszawski)

  SAT solvery

  SAT-solver, jaki jest, każdy widzi. Ale nie każdy przygląda się uważnie. Dlatego zamierzam opowiedzieć, co to dokładnie jest SAT-solver i jakie problemy można za pomocą takowego rozwiązywać  Postaram się omówić dość szczegółowo architekturę CDCL, czyli najpopularniejszy ostat...

Strony