Weryfikacja wspomagana komputerowo

Wykład poświęcony jest metodom weryfikacji pozwalającym na zwiększenie niezawodności systemów komputerowych. Omówione zostaną trzy podejścia: weryfikacja modelowa (ang. model-checking), dowodzenie poprawności programów i analiza statyczna (ang.static analysis). Pierwsza z nich odniosła już sukces przemysłowy w weryfikacji układów sprzętowych; połączenie dwóch pozostałych pozwala odnaleźć rozsądny kompromis pomiędzy siłą metody a jej efektywnością, i wydaje się być najlepsze w weryfikacji programów. W ramach wykładu omówione zostaną podstawy teoretyczne i algorytmy. W czasie laboratorium studenci zapoznają się z kilkoma narzędziami: SPIN, NuSMV, CBMC, Why3. Wykonają też własne projekty, co pozwoli lepiej zrozumieć treść wykładu.