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.

Description in English
The aim of this project consists in creating documents which clarify theoretical frame of the area of verification of programs handling with dynamic data structures, introduce chosen verification tools, include tutorials explaining work with these tools and demonstrate their functionality on proper examples. Two excersises of the Formal analysis and verification course will be based on these documents which will also be available on the website, so that they can be used even with students, which concentrate on data structures, or bachelor students which interest in formal verification.

Keywords
formální verifikace, dynamické datové struktury

Key words in English
formal verification, dynamic data structures

FR3101/2006/G1

Czech

Erlebach Pavel, Ing., Ph.D. - principal person responsible

Department of Intelligent Systems
- responsible department (1.1.1989 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (31.1.2006 - 31.12.2006)
Department of Intelligent Systems
- co-beneficiary (31.1.2006 - 31.12.2006)

Responsibility: Erlebach Pavel, Ing., Ph.D.