Project detail

Automata and Logic for Symbolic Verification of Software

Duration: 01.01.2010 — 31.12.2011

Funding resources

Ministerstvo školství, mládeže a tělovýchovy ČR - KONTAKT

- whole funder (2010-01-01 - 2011-12-31)

On the project

Automates et Logique pour la vérification symbolique de logiciels.

Description in Czech
Mezi techniky, které jsou určeny pro verifikaci nekonečně stavových systémů, patří přístupy založené na využití tzv. řezů, automatizované indukce, či symbolické verifikace, která je pravděpodobně nejběžnější a která je také předmětem tohoto projektu. Symbolická verifikace je založena na konečné reprezentaci množin stavů zkoumaných systémů (příp. jejích abstrakcí) pomocí vhodného formalismu. Mezi nejběžněji používané formalismy pro symbolickou reprezentaci množin stavů patří logiky a automaty.

Vědeckým cílem projektu je významně přispět ke zlepšení obecnosti a škálovatelnosti současných symbolických metod verifikace nekonečně stavových programů založených na využití logik a/nebo automatů. Za tím účelem budou jednak zkoumány možnosti zlepšení jednotlivých přístupů založených na logikách nebo automatech, velká pozornost však bude věnována také možnostem kombinace výhod obou těchto přístupů. Výzkum se přitom soustředí zejména na verifikaci programů s neomezenými celočíselnými proměnnými, poli a/nebo dynamickými datovými strukturami založenými na ukazatelích.

Mark

MEB021023

Default language

French

People responsible

Radu Iosif - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - principal person responsible

Units

Faculty of Information Technology
- beneficiary (2010-01-01 - 2011-12-31)

Results

BOZGA, M.; IOSIF, R.; KONEČNÝ, F. Fast Acceleration of Ultimately Periodic Relations. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2010. p. 227-242. ISBN: 978-3-642-14294-9.
Detail

ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.; BOUAJJANI, A. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, 2012, vol. 14, no. 2, p. 167-191. ISSN: 1433-2779.
Detail

HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6806, p. 424-440. ISSN: 0302-9743.
Detail

ŠIMÁČEK, J.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.: fapointers; Forester: A Tool for Verification of Programs with Pointers. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/forester/. URL: https://www.fit.vut.cz/research/product/142/. (software)
Detail

Responsibility: Rogalewicz Adam, doc. Mgr., Ph.D.