Topic of PhD thesis

Advisor:Vojnar Tomáš, prof. Ing., Ph.D.
Student:Konečný Filip, Ing.
Topic:Symbolic Verification Based on Extended Automata and Related Formalisms -- double degree study (cotutelle) with VERIMAG, Grenoble (dr. R. Iosif)
Start:2008/2009
Date of Defense:2012-10-29
Title of Dissertation:Relational Verification of Programs with Integer Data
PhD thesis subject:

Automatizovaná formální verifikace je moderním a rychle se rozvíjejícím přístupem k ověřování korektnosti počítačových systémů. Značná pozornost je jí věnována nejen v akademické oblasti, ale také řadou špičkových průmyslových společností působících v oblasti hardware (např. Intel, IBM), počítačových protokolů a sítí, vestavěných řídících systémů (např. pro potřeby palubních řídících systémů NASA) a v neposlední řadě také operačních systémů (zde se v současnosti stále více angažuje firma Microsoft a její divize Microsoft Research). Přes tento zájem univerzit i průmyslových společností je však v oblasti formální verifikace stále zapotřebí vyřešit celou řadu teoretických i praktických problémů.

Předmětem disertační práce je konkrétně formální verifikace počítačových programů s různými rysy nekonečnosti v datech a/nebo chování, jako jsou např. práce s neomezenými číselnými proměnnými, poli, dynamickými datovými strukturami, rekurzí, paralelismem, parametrizací apod. Důraz bude kladen na rozvoj metod symbolické verifikace s cílem zvýšit její obecnost a efektivnost, a to zejména při využití různých rozšířených typů automatů, jako jsou např. automaty s čítači.

Práce je řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou verifikací. Jedná se přitom o dvojí vedení (cotutelle/double degree) s VERIMAG, Grenoble (dr. R. Iosif).

Part of research project:
Related publications:
2007HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Berlin: Springer Verlag, 2007, pp. 145-161. ISBN 978-3-540-75595-1.
 VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. Brno: Faculty of Information Technology BUT, 2007. ISBN 978-80-214-3547-6.
 ČEŠKA Milan, ERLEBACH Pavel and VOJNAR Tomáš. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing. London: Springer London, 2007, vol. 19, no. 3, pp. 363-374. ISSN 0934-5043.
2006BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre and VOJNAR Tomáš. Programs with Lists are Counter Automata. In: Computer Aided Verification. Berlin: Springer Verlag, 2006, pp. 517-531. ISBN 978-3-540-37406-0.
 HABERMEHL Peter, IOSIF Radu and VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer Verlag, 2006, pp. 350-364. ISBN 978-3-540-33056-1.
2005BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre and VOJNAR Tomáš. Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer Verlag, 2005, pp. 13-29. ISBN 978-3-540-25333-4.
 HABERMEHL Peter and VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science. 2005, vol. 138, no. 3, pp. 21-36. ISSN 1571-0661.
2004BOUAJJANI Ahmed, HABERMEHL Peter and VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science. 2004, vol. 2004, no. 3114, pp. 372-386. ISSN 0302-9743.