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

Popis česky
Přestože již bylo navrženo několik různých přístupů k automatizované verifikaci (či statické analýze) programů s dynamickými datovými strukturami provázanými ukazateli, tyto přístupy stále zůstávají daleko od toho, aby byly dostatečně obecné (tj. pokrývaly všechny podoby dynamických datových struktur, s nimiž se setkáváme v praxi), aby byly plně automatizované a aby byly současně efektivní. Cílem tohoto projektu je proto přispět co největší mírou k rozvoji současného stavu poznání v oblasti automatizované verifikace programů s dynamickými datovými strukturami směrem k navržení technik, které by lépe plnily výše uvedená kritéria. Způsob, jakým projekt zamýšlí dosáhnout výše uvedeného cíle, je založen především na rozvoji metody označované jako tzv. abstraktní regulární model checking (abstract regular model checking).

Klíčová slova
vérification automatique, systčmes infinis, regular model checking, programmes avec structures de données  dynamiques ŕ pointeurs,

Klíčová slova česky
formální verifikace, nekonečně stavové systémy, regulární model checking, programy s dynamickými datovými strukturami

2-06-27

francouzština

Vojnar Tomáš, prof. Ing., Ph.D. - hlavní řešitel
Bouajjani Ahmed - spoluřešitel
Češka Milan, prof. RNDr., CSc. - spoluřešitel
Erlebach Pavel, Ing., Ph.D. - spoluřešitel
Holík Lukáš, doc. Mgr., Ph.D. - spoluřešitel
Moro Pierre - spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. - spoluřešitel
Touili Tayssir, Dr., Ph.D. - spoluřešitel

Ústav inteligentních systémů
- odpovědné pracoviště (1.1.1989 - nezadáno)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT
- interní (2.2.2006 - 31.12.2007)
Ústav inteligentních systémů
- spolupříjemce (2.2.2006 - 31.12.2007)

Odpovědnost: Vojnar Tomáš, prof. Ing., Ph.D.