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

Agency: Barrande - Czech-French programme of integrated actions



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


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. (UITS FIT VUT) , research leader
Habermehl Peter (UPAR7) , team leader
Bouajjani Ahmed (UPAR7)
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Erlebach Pavel, Ing. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Moro Pierre (LIAFA UP7/CNRS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Touili Tayssir (LIAFA UP7/CNRS)




Back to top