I. Tematy raczej praktyczne
Zastosowanie (hierarchicznej) agregacji w stochastycznej weryfikacji modelowej
| Probabilistyczna weryfikacja modelowa (ang. probabilistic model-checking) to metoda weryfikacji modeli probabilistycznych, takich jak łańcuch Markowa. Oprócz aspektu jakościowego (coś się wydarzy lub nie) mamy tu na ogół do czynienia również z aspektem ilościowym (coś się wydarzy z jakimś prawdopodobieństwem), dlatego weryfikacja modelowa wymaga rozwiązywania układów równań liniowych. Używane są najczęściej algorytmy iteracyjne, tak jest np. w narzędziu PRISM. Celem pracy jest dokończenie implementacji algorytmu opartego na hierarchicznej agregacji, zaproponowanego w pracy doktorskiej P. Pokarowskiego, zintegrowanie tego algorytmu z narzędziem PRISM, oraz eksperymentalna ewaluacja tego rozszerzenia na wybranych case-studies. |
Sprawdzanie równoważności programów
| Rozwinięcie pomysłu z pracy magisterskiej z zeszlego roku, w której zaadaptowano metodę ograniczonej weryfikacji modelowej, w wydaniu zaimplementowanym w narzędziu CBMC, do znajdowania nierównoważności prostych programów w C. Jako wynik uzyskuje się wykonania dwóch programów, dające różne wyniki dla tych samych danych wejściowych (o ile takie odróżniające wykonania istnieją, i o ile są one wystarczająco krótkie). Narzędzie to zostało zintegrowane z plarformą Codility, służącą do egzaminowania programistów za pomocą prostych zadań programistycznych, i zostało użyte do znaleznienia błędów w rozwiązaniach dotychczas uznawanych przez Codility za poprawne. Celem niniejszej pracy jest powtórzenie opisanego wyżej procesu dla języka Java. Można też pomyśleć o tranlacji do kodu pośredniego, wspólnego dla wielu języków. |
Weryfikacja programów binarnych
| Kontunuacja pracy magisterskiej z zeszłego roku. Celem pracy jest opracowanie metody weryfikacji programów w sytuacji, gdy dysponujemy tylko kodem binarnym, a kod źródłowy jest niedostępny. Użyjemy (i zaadaptujemy) narzędzie CBMC, służące do weryfikacji programów w C. Praca polegać będzie na zastąpieniu języka wejściowego CBMC przez język maszynowy, lub jego rozsądny podzbiór, wybranego procesora. |
Usprawnienie weryfikacji programów wskaźnikowych
| Kontunuacja pracy magisterskiej z zeszłego roku. W jej wyniku powstało rozszerzenie narzędzia CBMC, usprawniające weryfikację programów operujących na wskaźnikach. Usprawnienie to zachowuje poprawność weryfikacji przy założeniu deterministycznych wskaźników, czyli wtedy, gdy adres odwołania do pamięci jest zawsze jednoznaczny (deterministyczny). (W CBMC, jednym ze źródeł niedeterminizmu są dane wejściowe weryfikowanego programu.) Celem pracy jest eksperymentalne porównanie orginalnego CBMC i jego usprawnionej wersji. Prawdopodobnie będzie też konieczne poprawnienia analizy wskaźników wykonywanej w CBMC, w celu wykorzystania w pełni możliwości oferowanych przez determinizm wskaźników. |
II. Tematy raczej teoretyczne
(osoby zainteresowane proszę o kontakt indywidualny)
S. Lasota (2012.04.28)