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

Formal verification of programs working with dynamic data strucktures

grant

formal verification, dynamic data structures

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.

Erlebach Pavel, Ing., Ph.D. – research leader
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)