Detail projektu

Automates et Logique pour la vérification symbolique de logiciels

Období řešení: 1. 1. 2010 – 31. 12. 2011

Typ projektu: grant

Kód: MEB021023

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

Program: KONTAKT

Název anglicky
Automata and Logic for Symbolic Verification of Software
Název česky
Automaty a logiky v symbolické verifikaci software
Typ
grant
Klíčová slova

formální verifikace, nekonečně stavové systémy, symbolické reprezentace,
automaty, logiky

Abstrakt

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.

Řešitelé
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS) – hlavní řešitel
Bozga Marius
Habermehl Peter
Konečný Filip, Ing., Ph.D.
Radu Iosif
Šimáček Jiří, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Publikační výsledky

2012

  • 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

2011

  • 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

2010

  • 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
Aplikované výsledky

2010

Ostatní výsledky

2011

Nahoru