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.

MEB021023

French

Rogalewicz Adam, doc. Mgr., Ph.D. - principal person responsible
Bozga Marius - fellow researcher
Habermehl Peter - fellow researcher
Konečný Filip, Ing., Ph.D. - fellow researcher
Šimáček Jiří, Ing., Ph.D. - fellow researcher
Vojnar Tomáš, prof. Ing., Ph.D. - fellow researcher

Department of Intelligent Systems
- responsible department (17.3.2010 - not assigned)
Faculty of Information Technology
- responsible department (1.1.1989 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (17.3.2010 - 31.12.2011)
Department of Intelligent Systems
- co-beneficiary (17.3.2010 - 31.12.2011)
Laboratoire d'Informatique Algorithmique: Fondements et Applications
- co-beneficiary (17.3.2010 - 31.12.2011)
VERIMAG
- co-beneficiary (17.3.2010 - 31.12.2011)
Faculty of Information Technology
- beneficiary (1.1.2010 - 31.12.2011)

HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011. p. 0-0.
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

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

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