Téma disertační práce

Školitel:Vojnar Tomáš, prof. Ing., Ph.D.
Téma:Symbolická verifikace s využitím rozšířených automatů a příbuzných formalismů -- společné vedení (double degree/cotutelle) s VERIMAG, Grenoble (dr. R. Iosif)
Zahájení v ak.r.:2008/2009
Obhajoba disertace:2012-10-29
Název disertace:Relační verifikace programů s celočíselnými daty
Charakteristika řešeného problému:

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).

Součást výzkumného projektu:
Publikace související s vypsaným tématem:
2007HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Berlin: Springer Verlag, 2007, s. 145-161. ISBN 978-3-540-75595-1.
 VOJNAR Tomáš. Cut-offs and Automata in Formal Verification of Infinite-State Systems. Brno: Fakulta informačních technologií VUT v Brně, 2007. ISBN 978-80-214-3547-6.
 ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. Formal Aspects of Computing. London: Springer London, 2007, roč. 19, č. 3, s. 363-374. ISSN 0934-5043.
2006BOUAJJANI Ahmed, BOZGA Marius, HABERMEHL Peter, IOSIF Radu, MORO Pierre a VOJNAR Tomáš. Programs with Lists are Counter Automata. In: Computer Aided Verification. Berlin: Springer Verlag, 2006, s. 517-531. ISBN 978-3-540-37406-0.
 HABERMEHL Peter, IOSIF Radu a 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, s. 350-364. ISBN 978-3-540-33056-1.
2005BOUAJJANI Ahmed, HABERMEHL Peter, MORO Pierre a 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, s. 13-29. ISBN 978-3-540-25333-4.
 HABERMEHL Peter a VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science. 2005, roč. 138, č. 3, s. 21-36. ISSN 1571-0661.
2004BOUAJJANI Ahmed, HABERMEHL Peter a VOJNAR Tomáš. Abstract Regular Model Checking. Lecture Notes in Computer Science. 2004, roč. 2004, č. 3114, s. 372-386. ISSN 0302-9743.

Vaše IPv4 adresa: 34.204.189.171
Přepnout na https