Tematy prac

• 1. Zastosowanie "SAT-testerów" w teorii gier.
• SAT-solvery to najnowsze narzędzia, które często b. efektywnie rozwiązuja problem spełnialnosci formuł zdaniowych. Wykorzystywane sa w wielu dziedzinach, gdzie mamy do czynienia z problemami NP-trudnymi. Zadaniem jest wykorzystanie tych algorytmów do poszukiwania optymalnych strategii w wybranych grach.
• 2. Algorytmiczne metody testowania spelnialnosci formul zdaniowych (SAT).
• 3. Analiza porownawcza SAT-testerów.
• 4. Projektowanie i implementacja metod weryfikacji modelowej dla logik epistemicznych.
• Logiki epistemiczne oprocz operatorów temporalnych zawierają też operatory wiedzowe. Zadaniem jest zaimplementowanie znanych algorytmów sprawdzających czy formuła jest prawdziwa w modelu. Praca będzie stanowić czesc dużego systemu weryfikacyjnego VerICS. http://www.ipipan.waw.pl/~penczek/abmpw/index.htm
• 5 Parametryczna weryfikacja modelowa przy uzyciu narzędzia UppAll.
• 6. Parametryczna weryfikacja modelowa: metody i algorytmy.
• 7. Multimedialny podrecznik do programowania w Promeli.
• 8 Wizualizacja kontrprzykładów dla weryfikatora systemów w Promeli.
• 9 Baza protokołów w Promeli i translacje do TADD i do Uppalla.
• 10 Interfejs graficzny w C++ dla weryfikatora programów w Promeli.
• 11 Metody kompozycji aplikacji i procesów biznesowych.
• 12 Metody opisu ontologii w architekturach SOA.