Tematem seminarium są modele matematyczne, metody, algorytmy i narzędzia pozwalające na zwiększenie niezawodności oprogramowania. Skupimy się przede wszystkim na analizie programów współbieżnych oraz obiektowych.

Centralną tematyką seminarium jest niezawodność systemów informatycznych, obejmująca takie aspekty systemu jak poprawność funkcjonalna, bezpieczeństwo, efektywność, jakość oprogramowania, itp. Naszą motywacją jest obserwowany ostatnio systematyczny wzrost zainteresowania przemysłu metodami pozwalającymi na zwiększenie niezawodność programów. Tematem seminarium są modele matematyczne, metody, algorytmy i narzędzia temu służące. Dalekosiężnym celem seminarium jest opracowanie nowych metod i zbudowanie własnych narzędzi, np. w ramach doktoratu, więc serdecznie zapraszamy osoby zainteresowane studiami doktoranckimi. Ze względu na ich wagę i powszechność, koncentrujemy się przede wszystkim na dwóch kategoriach systemów informatycznych:
  • systemy współbieżne i rozproszone;

  • systemy obiektowe.
Tematyka seminarium obejmuje m.in.:
  • matematyczne modele systemów współbieżnych i rozproszonych (sieci Petriego, rozszerzone automaty, algebra procesów, itp.);

  • języki specyfikacji własności programów;

  • metody weryfikacji formalnej wspomaganej komputerowo: analiza statyczna, weryfikacja modelowa (ang. model checking), dowodzenie poprawności, analiza dynamiczna, testowanie;

  • problemy decyzyjne w weryfikacji (np. osiągalność/niepustość, terminacja, ograniczoność, żywotność) -- rozstrzygalność, algorytmy i złożoność obliczeniowa;

  • elementy teorii automatów (automaty czasowe, omega-automaty, automaty na słowach z danymi, itp);

  • narzędzia do weryfikacji.