Detail projektu

Automates et Logique pour la vérification symbolique de logiciels

Období řešení: 01.01.2010 — 31.12.2011

Zdroje financování

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

- plně financující (2010-01-01 - 2011-12-31)

O projektu

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

Popis česky
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.

Označení

MEB021023

Originální jazyk

francouzština

Řešitelé

Rogalewicz Adam, doc. Mgr., Ph.D. - hlavní řešitel
Radu Iosif - spoluřešitel

Útvary

Fakulta informačních technologií
- příjemce (01.01.2010 - 31.12.2011)

Výsledky

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

Odpovědnost: Rogalewicz Adam, doc. Mgr., Ph.D.