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.