Propozycje A. Schuberta tematów prac magisterskich.
I. Tematy raczej praktyczne
Napisanie mechanizmu sprawdzania typów dla naiwnej teorii typów połączone z zakodowaniem while-programów
Na naszym wydziałe obecnie tworzona jest nowa logika pozwalająca na tworzenie dowodów twierdzeń w bardzo naturalny sposób. W tej chwili opracowane są teoretyczne podstawy znaczącej części tej logiki. Warto jednak byłoby do tych teoretycznych podstaw dodać narzędzie pozwalające na automatyczne sprawdzanie, czy podany dowód zgadza się z regułami tej logiki. Proponujemy napisanie takiego narzędzia uzupełnionego o podstawowe mechanizmy weryfikacji while-programów.
Praca ta może być wstępem nawet do późniejszej pracy doktorskiej polegającej na rozwinięciu tej implementacji do pełnego systemu wspomagania dowodzenia twierdzeń.
Plugin do Eclipse wspomagający pisanie i rozumienie programów w bajtkodzie Javy
Pisanie programów w bajtkodzie Javy jest trudne, gdyż bajtkod jest językiem niskopoziomowym. Czasami jednak pojawia się konieczność zrozumienia, co dany fragment kodu dostępny tylko w postaci niskopoziomowej właściwie robi. Dostępność narzędzi wspomagających proces rozumienia takiego kodu podniosłaby jakość tworzonego oprogramowania. Proponujemy wzbogacenie istniejącego już narzędzie Umbra o nowe funkcje pomagające programiście w rozumieniu analizowanego kodu.
Wykonanie tej pracy powinno być doskonałym źródłem wiedzy na temat bajtkodu Javy oraz tajników budowy plików klasowych Javy. W niektórych wariantach może stanowić punkt wyjścia do pracy doktorskiej.
Narzędzie do wykonywania analizy statycznej lub typowania programów
Chcielibyśmy, aby środowisko Umbry było wyposażone dodatkowo w mechanizmy pozwalające na stwierdzanie poprawności programów zapisanych w bajtkodzie Javy. Przez poprawny program będziemy tutaj rozumieli program spełniający określoną własność. Proponujemy w ramach pracy magisterskiej wzbogacenie istniejących mechanizmów Umbry o sprawdzanie właśności takich jak:
Wykonanie tej pracy powinno być doskonałym źródłem wiedzy na temat bajtkodu Javy oraz tajników budowy plików klasowych Javy. Dodatkowo w wyniku jej wykonania nabędzie się doświadczenia w zakresie problemów spotykanych przy projektowaniu i tworzeniu programów w Javie. W niektórych wariantach może stanowić punkt wyjścia do pracy doktorskiej.
Realizacja systemu typów gwarantującego funkcyjność metod
W ramach wcześniejszych badań udało się nam opracować system typów gwarantujący iż dana metoda jest funkcją, przy czym funkcyjność rozumiemy tutaj jako zachodzenie łączne dwóch warunków:
W ramach pracy magisterskiej proponujemy stworzenie narzędzia, które z użyciem adnotacji Javowych zgodnych ze standardem JSR 308 będzie pozwalało na sprawdzanie funkcyjności metod.
Wykonanie tej pracy powinno być doskonałym źródłem wiedzy na temat bajtkodu Javy oraz tajników budowy plików klasowych Javy. W szczególności zdobywać się tutaj będzie wiedzę na temat nowego standardu jawowego - JSR 308. Znajomość tego standardu może być przydatna w przemyśle, ale też i przy ewentualnym pisaniu doktoratu polegającego na tworzeniu narzędzi w oparciu o tę technikę.
Weryfikacja poprawności biblioteki kryptograficznej w Javie
Biblioteki kryptograficzne są powszechnie używane do zabezpieczania danych w różnego rodzaju programach. W związku z tym sam ich kod powinien odznaczać się wysoką jakością i powinien budzić zaufanie. Proponujemy dokonanie weryfikacji bezbłędności oraz przynajmniej częściowej weryfikacji własności funkcyjnych dla wybranej biblioteki procedur kryptograficznych z dostępnym otwartym kodem źródłowym.
W wyniku wykonania tej pracy autor pozna dogłębnie implementacje procedur kryptograficznych oraz zaznajomi się z gwarancjami bezpieczeństwa dawanymi przez nie. Dodatkowo zapozna się z możliwymi błędogennymi konstrukcjami, jakie mogą się pojawiać w tego rodzaju implementacjach.
Analiza bezpieczeństwa wybranej aplikacji napisanej w Javie lub C
Analiza bezpieczeństwa zastosowanego rozwiązania informatycznego jest bardzo skomplikowanym zadaniem. Zajęcie to wymaga doświadczenia i dokładnej znajomości wielu niuansów związanych z używanymi platformami i narzędziami. Proponujemy dokonanie wyboru aplikacji i przeprowadzenie dosyć szczegółowej analizy bezpieczeństwa zastosowanych w niej rozwiązań proceduralnych oraz stworzonego kodu.
W wyniku wykonania tej pracy autor pozna dogłębnie implementację wybranej aplikacji, co może być przydatne w dalszej karierze w przemyśle. Dodatkowo zapozna się z możliwymi błędogennymi konstrukcjami, jakie mogą się pojawiać w tego rodzaju implementacjach.
Wspomaganie weryfikacji programów w Javie przy użyciu Coq-a
Coq jest systemem wspomagającym dowodzenie twierdzeń. Można go używać do weryfikacji poprawności programów względem zadanej specyfikacji. Jednak opracowanie takiego dowodu jest bardzo pracochłonne. Proponujemy pracę polegającą na wykonaniu weryfikacji prostego kawałka programu, zaproponowanie usprawnienia do Coq-a, ułatwiającego dowodzenie poprawności programów, a następnie zrealizowanie tego usprawnienia.
W wyniku wykonania tej pracy autor pozna dogłębnie weryfikowany algorytm. Zaproponowane usprawnienie, jeśli będzie interesujące, może stanowić punkt wyjścia do tworzenia pracy doktorskiej.
Formalny opis protokołu
Dokumenty RFC są doskonałym źródłem napisanych w języku naturalnym specyfikacji. Fakt, iż dokumenty te zostały stworzone w języku naturalnym sprawia, iż możliwe że zawierają one wewnętrzne sprzeczności. Proponujemy wykonanie formalnego opisu wybranego protokołu w jakimś języku formalnym, a następnie użycie narzędzi do wykrycia, czy nie ma jakichś niespójności w uzyskanej formalizacji. Może to pomóc w wynalezieniu niespójności i błędów specyfikacyjnych.
W wyniku wykonania tej pracy autor pozna dogłębnie formalizowany protokół.
Eksperymentalna ocena narzędzia Caduceus, Krakatoa, KeY
Caduceus, Krakatoa i KeY są narzędziami do dokonywania formalnej weryfikacji programów. Pozwalają one na stwierdzenie, czy dana realizacja programistyczna rzeczywiście odpowiada oczekiwaniom opisanym w formalnej specyfikacji. Proponujemy pracę zmierzającą do ocenienia, na ile wybrane spośród wyżej wymienionych narzędzi nadaje się do pracy typowego programisty.
W wyniku wykonania tej pracy autor pozna dogłębnie w/w narzędzia. Może okazać się to pożyteczne przy podejmowaniu studiów doktoranckich. Być może w przyszłości tego rodzaju narzędzia będą też stosowane w przemyśle. Odpowiednio przygotowany materiał może tutaj być podstawą do publikacji naukowej.
II. Tematy raczej teoretyczne
Logika intuicjonistyczna i automaty na drzewach
Zdaniowa logika drugiego rzędu w wersji intuicjonistycznej jest w ogólności interpretowana na strukturach Kripkego. W pewnym uproszczeniu struktury te są częściowymi porządkami. Można rozważać taką logikę, tak jak to się robi z logiką pierwszego rzędu, tylko na wybranych modelach. Interesującym przypadkiem jest tutaj sytuacja, gdy rozważany porządek częściowy jest drzewem. Wiadomo, że taka logika daje się sprowadzić do logiki S\omega S (monadycznej logiki drugiego rzędu na drzewach). Ta logika jest rozstrzygalna i bardzo często pojawia się w kontekście weryfikacji systemów współbieżnych. Proponuję na temat pracy magisterskiej bliższe przyjrzenie się tej logice. Można tutaj po prostu spróbować pobawić się i wskazać, jakie właśności współbieżne wyrażają się w takiej logice intuicjonistycznej. Inny nurt polegałby na powtórzeniu konstrukcji z twierdzenia Rabina i określeniu, jaka jest złożoność problemu sprawdzania spełnialności formuł takiej logiki.
W wersji bardziej ambitnej praca ta może stanowić podstawę do publikacji, a w dalszej perspektywie doktoratu.
Automaty drzewowe z warunkami równościowymi
W literaturze istnieje pojęcie automatu z warunkami równościowymi. W automacie takim w pewnych stanach oprócz symbolu w wierzchołku drzewa oraz stanów w synach drzewa sprawdzana jest również równość wybranych poddrzew. W ogólności tego rodzaju automaty mają nierozstrzygalny problem niepustości sprawdzanego przez nie języka drzew. Jednak w istnieją ograniczenia tego modelu obliczeń, w których niepustość jest rozstrzygalna. W ramach niedawnych badań udało się pokazać rozstrzygalność niepustości dla pewnej nowej klasy tego rodzaju automatów. Interesujące byłoby stwierdzenie, czy ta klasa ma także odpowiednie własności zamkniętości (zamkniętość na koniunkcję, alternatywę, rzutowanie i negację). Proponuję w ramach pracy magisterskiej opracowanie właśnie konstrukcji domknięcia dla tej nowej klasy automatów.
W wersji bardziej ambitnej praca ta może stanowić podstawę do publikacji, a w dalszej perspektywie doktoratu.
Algorytmy automatycznego wykrywania reprezentacji
We współczesnych badaniach nad Javą pojawia się często temat opisu koncepcyjnej reprezentacji danego obiektu rozciągającej się na wiele innych obiektów obecnych na stercie. Jednak opis taki wymaga wprowadzenia dodatkowych adnotacji w kodzie. Ich wprowadzanie może być trudne i żmudne. Chcielibyśmy zaproponować opracowanie kilku użytecznych taktych pozwalających na automatyczne wykrywanie, jakie konkretnie obiekty przynależą do reprezentacji zadanego obiektu.
Algorytmy sprawdzania braku NullPointerException
Ostatnio pojawiło się wiele ciekawych metod pozwalających na unikanie NullPointerException w produkowanym kodzie. Metody te opierają się na wprowadzaniu adnotacji do kodu źródłowego. Chcielibyśmy zaproponować pracę porównującą te metody oraz opracowującą nowe algorytmy sprawdzania, czy kod jest wolny od NullPointerException i/lub generowania adnotacji wspomagających wykrywanie, że takie wyjątki nie występują.
Wyprowadzanie informacji o aliasach
W typowej aplikacji jawowej dany obiekt może znajdować się pod wieloma zmiennymi obecnymi w systemie. Istnieje wiele sposobów zarządzania tym, jakie zmienne mogą zawierać wspólną referencję (być aliasami obiektu). Zarządzanie to jednak wymaga zwykle wprowadzania dodatkowych informacji do kodu źródłowego (np. tego, jakie zmienne są modyfikowane w treści metody). Chcielibyśmy zaproponować pracę polegającą na opracowaniu metody wyprowadzania tego rodzaju adnotacji dla wybranego formalizmu zarządzania aliasami.