Project Details

Vérification automatique de programmes avec structures de données dynamiques a pointeurs

Project Period: 1. 1. 2006 – 31. 12. 2007

Project Type: grant

Code: 2-06-27

English title
Automatic Verification of Programs with Dynanic Data Structures with Pointers
Czech title
Automatická verifikace programů s dynamickými datovými strukturami provázanými ukazateli
Type
grant
Keywords

formal verification, infinite-state systems, regular model checking, programs with dynamic linked data structures

Abstract

Though there have already been proposed multiple approaches to
automatic formal verification (or static analysis) of programs with
pointers and dynamic linked data structures, these approaches are still
far from being general (i.e. covering all the different shapes of
structures that one may encounter in practice), fully automatic, and at
the same time efficient. The goal of the present project is thus to
push the current state-of-the-art in the given area as far as possible
towards obtaining techniques for automated verification of programs
with dynamic linked data structures that would meet the above described
criteria. The way the project intends to achieve the above goal is
primarily based on a further development of the abstract regular model
checking (ARMC) framework proposed by A. Boujjani, P. Habermehl, and T.
Vojnar at CAV 2004.

Team members
Vojnar Tomáš, prof. Ing., Ph.D. (DITS) – research leader
Bouajjani Ahmed
Češka Milan, prof. RNDr., CSc.
Erlebach Pavel, Ing., Ph.D.
Habermehl Peter
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Moro Pierre
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Touili Tayssir, Dr., Ph.D.
Back to top