Automates et Logique pour la vérification symbolique de logiciels

Automata and Logic for Symbolic Verification of Software

Automaty a logiky v symbolické verifikaci software

grant

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

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.

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)