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: Barrande - česko-francouzský program integrovaných akcí

Program: KONTAKT

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 FIT VUT) , hlavní řešitel
Iosif Radu (VERIMAG) , spoluřešitel
Bozga Marius (VERIMAG)
Habermehl Peter (UPAR7)
Konečný Filip, Ing. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Publikace

2012

  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, roč. 14, č. 2, 2012, s. 167-191. ISSN 1433-2779. Detail

2011

  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, roč. 2011, č. 6806, s. 424-440. ISSN 0302-9743. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail

2010

  • BOZGA Marius, IOSIF Radu a KONEČNÝ Filip. Fast Acceleration of Ultimately Periodic Relations. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 6174. Berlin: Springer Verlag, 2010, s. 227-242. ISBN 978-3-642-14294-9. Detail
Produkty

2010

  • Forester: Nástroj pro verifikaci programů s ukazateli, software, 2010
    Autoři: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš Detail
Nahoru