Project detail

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

Duration: 01.01.2006 — 31.12.2007

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 (2006-01-01 - 2007-12-31)
Češka Milan, prof. RNDr., CSc.
- fellow researcher (2006-01-01 - 2007-12-31)
Erlebach Pavel, Ing., Ph.D.
- fellow researcher (2006-01-01 - 2007-12-31)
Habermehl Peter
- fellow researcher (2006-01-01 - 2007-12-31)
Holík Lukáš, Mgr., Ph.D.
- fellow researcher (2006-01-01 - 2007-12-31)
Rogalewicz Adam, doc. Mgr., Ph.D.
- fellow researcher (2006-01-01 - 2007-12-31)

Units

Department of Intelligent Systems
- (2006-01-01 - 2007-12-31)

Results

ROGALEWICZ, A. Verification of Programs with Complex Data Structures. Brno: 2007. 122 p. ISBN: 978-80-214-3548-3.
Detail

HOLÍK, L., VOJNAR, T., ABDULLA, P., BOUAJJANI, A., KAATI, L. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno: 2008.
Detail

HOLÍK, L., VOJNAR, T., ABDULLA, P., KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno: 2008.
Detail