Formální verifikace programů pracujících s dynamickými datovými strukturami

Formal verification of programs working with dynamic data strucktures

grant

formální verifikace, dynamické datové struktury

Cílem tohoto projektu je vytvořit dokumenty, které vysvětlují teoretický rámec oblasti verifikace programů pracujících s dynamickými datovými strukturami, představují vybrané verifikační nástroje, naznačují způsob práce s nimi formou tutorialů a umožňují zájemcům vyzkoušet jejich funkčnost na vhodných příkladech. Tyto dokumenty budou sloužit jako podklady pro dvě cvičení do předmětu Formální analýza a verifikace, zároveň budou volně dostupné prostřednictvím webových stránek, takže je budou moci využívat např. i studenti zabývající se datovými strukturami, nebo studenti bakalářského studia, kteří se zajímají o verifikaci a mají bakalářskou práci zaměřenou na tuto oblast, ale nemohou si ještě zapsat zmiňovaný magisterský předmět.

Erlebach Pavel, Ing., Ph.D. – hlavní řešitel
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)