Project detail
Automatic Verification of Programs with Dynanic Data Structures with Pointers
Duration: 1.1.2006 — 31.12.2007
Funding resources
On the project
Vérification automatique de programmes avec structures de données dynamiques ŕ pointeurs.
Description in Czech
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).
Keywords
vérification automatique, systčmes infinis, regular model checking, programmes
avec structures de données dynamiques ŕ pointeurs,
Key words in Czech
formální verifikace, nekonečně stavové systémy, regulární model checking,
programy s dynamickými datovými strukturami
Mark
2-06-27
Default language
French
People responsible
Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsible
Bouajjani Ahmed - fellow researcher
Češka Milan, prof. RNDr., CSc. - fellow researcher
Erlebach Pavel, Ing., Ph.D. - fellow researcher
Holík Lukáš, doc. Mgr., Ph.D. - fellow researcher
Moro Pierre - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher
Touili Tayssir, Dr., Ph.D. - fellow researcher
Units
Department of Intelligent Systems
- responsible department (1.1.1989 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (2.2.2006 - 31.12.2007)
Department of Intelligent Systems
- co-beneficiary (2.2.2006 - 31.12.2007)
Responsibility: Vojnar Tomáš, prof. Ing., Ph.D.