Prof. Ing. Tomáš Vojnar, Ph.D.

Pokročilé techniky automatické verifikace nekonečně stavových systémů
Hlavní řešitel:Vojnar Tomáš
Spoluřešitelé:Habermehl Peter
Další řešitelé:Bouajjani Ahmed, Češka Milan, Holík Lukáš, Rogalewicz Adam, Smrčka Aleš, Touili Tayssir
Agentura:BARRANDE
Kód:MEB 020840
Začátek:2008
Konec:2009
Klíčová slova:formální verifikace, nekonečně stavové systémy, model checking
Anotace:
Efektivita současných technik pro model checking nekonečně stavových systémů je však stále relativně daleko od jejich skutečně praktické aplikovatelnosti a také třídy systémů a jejich ověřovaných vlastností, na které se tyto techniky dají uplatnit, jsou omezené. Cílem tohoto projektu je proto přispět k výzkumu metod model checkingu nekonečně stavových systémů tak, aby byly v co největší míře odstraněny jejich současná omezení jak v oblasti efektivity, tak v oblasti obecnosti. S cílem zvýšit efektivitu současných technik symbolického model checkingu nekonečně stavových systémů budou v projektu konkrétně zkoumány např. techniky symbolického model checkingu založené na nedeterministických konečných automatech, jež by měly umožnit vyhnout se determinizaci, která je jedním z výpočetně nejdražších kroků v rámci současných přístupů. Za tím účelem je zapotřebí vyvinout všechny potřebné operace (jako např. ověřování prázdnosti, inkluze, minimalizace, abstrakce apod.) nad různými používanými typy automatů nad slovy, stromy atd. Pro zvýšení obecnosti současných technik pak projekt zahrne jak výzkum možností verifikace složitějších systémů (např. programů s neomezenými dynamickými datovými strukturami založenými na ukazatelích a současně s neomezenými celočíselnými proměnnými) i výzkum možností ověřování složitějších vlastností než dosud (včetně např. konečnosti výpočtu či vlastností typu živost). Při práci na tomto cíli budou zkoumány různá rozšíření současných automatů a logik (např. kombinace různých tříd automatů a logik popisujících kvalitativní strukturu systému s různými kvantitativními omezeními) a také algoritmy pro práci s takto rozšířenými formalismy, zahrnující např. pokročilé rozhodovací procedury nad logikami, nové metody abstrakce a učení nad automaty apod. Projekt přitom zahrne jak teoretický výzkum nových metod automatické verifikace nekonečně stavových systémů tak také prototypovou implementaci navržených technik tak, aby jejich vlastnosti mohly být ověřeny na vhodných případových studiích systémů s neomezenými a/nebo dynamickými strukturami, případně s parametry.

Produkty

Publikace

2011Holík Lukáš: Simulations and Antichains for Efficient Handling of Finite Automata, Brno, CZ, UITS FIT VUT, 2011, s. 128
2010Habermehl Peter, Iosif Radu, Vojnar Tomáš: Automata-based Verification of Programs with Tree Updates, In: Acta Informatica, roč. 47, č. 1, 2010, DE, s. 1-31, ISSN 0001-5903
2009Abdulla Parosh A., Bouajjani Ahmed, Holík Lukáš, Kaati Lisa, Vojnar Tomáš: Composed Bisimulation for Tree Automata, In: International Journal of Foundations of Computer Science, roč. 20, č. 4, 2009, SG, s. 685-700, ISSN 0129-0541
 Abdulla Parosh A., Holík Lukáš, Chen Yu-Fang, Vojnar Tomáš: Mediating for Reduction (On Minimizing Alternating Büchi Automata), Brno, CZ, FIT VUT, 2009, s. 26
 Abdulla Parosh A., Holík Lukáš, Chen Yu-Fang, Vojnar Tomáš: Mediating for Reduction (On Minimizing Alternating Büchi Automata), FIT-TR-2009-02, Brno, CZ, 2009, s. 29
 Abdulla Parosh A., Holík Lukáš, Chen Yu-Fang, Vojnar Tomáš: Zprostředkování pro redukci (Za minimalizací alternujících automatů), In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009), Wadern, DE, DROPS, 2009, s. 1-12, ISBN 978-3-939897-13-2
 Abdulla Parosh A., Holík Lukáš, Kaati Lisa, Vojnar Tomáš: A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata, In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, roč. 2009, č. 251, US, s. 27-48, ISSN 1571-0661
 Bozga Marius, Habermehl Peter, Iosif Radu, Konečný Filip, Vojnar Tomáš: Automatic Verification of Integer Array Programs, In: Computer Aided Verification, Berlin, DE, Springer, 2009, s. 157-172, ISBN 978-3-642-02657-7
 Bozga Marius, Habermehl Peter, Iosif Radu, Konečný Filip, Vojnar Tomáš: Automatic Verification of Integer Array Programs, TR-2009-2, Grenoble, FR, VERIMAG, 2009, s. 49
 Holík Lukáš, Šimáček Jiří: Optimizing an LTS-Simulation Algorithm, FIT-TR-2009-03, Brno, CZ, 2009, s. 17
 Holík Lukáš, Šimáček Jiří: Optimizing an LTS-Simulation Algorithm, In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Znojmo, CZ, FI MUNI, 2009, s. 93-101, ISBN 978-3-939897-15-6
 Iosif Radu, Rogalewicz Adam: Automata-Based Termination Proofs, In: Implementation and Application of Automata, Berlin, DE, Springer, 2009, s. 165-177, ISBN 978-3-642-02978-3
2008Abdulla Parosh A., Bouajjani Ahmed, Holík Lukáš, Kaati Lisa, Vojnar Tomáš: Composed Bisimulation for Tree Automata, In: Implementation and Application of Automata, Berlin, DE, Springer, 2008, s. 212-222, ISBN 978-3-540-70843-8
 Abdulla Parosh A., Holík Lukáš, Kaati Lisa, Vojnar Tomáš: A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata, In: 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Brno, CZ, FI MUNI, 2008, s. 3-11, ISBN 978-80-7355-082-0
 Bouajjani Ahmed, Habermehl Peter, Holík Lukáš, Touili Tayssir, Vojnar Tomáš: Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata, In: Implementation and Application of Automata, Berlin, DE, Springer, 2008, s. 57-67, ISBN 978-3-540-70843-8
 Bouajjani Ahmed, Habermehl Peter, Holík Lukáš, Touili Tayssir, Vojnar Tomáš: Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata, FIT-TR-2008-007, Brno, CZ, FIT VUT, 2008, s. 15
 Habermehl Peter, Iosif Radu, Vojnar Tomáš: A Logic of Singly Indexed Arrays, In: Logic for Programming, Artificial Intelligence and Reasoning, Berlin, DE, Springer, 2008, s. 558-573, ISBN 978-3-540-89438-4
 Habermehl Peter, Iosif Radu, Vojnar Tomáš: A Logic of Singly Indexed Arrays, TR-2008-9, Grenoble, FR, VERIMAG, 2008, s. 19
 Habermehl Peter, Iosif Radu, Vojnar Tomáš: What else is decidable about integer arrays?, TR-2007-8, Grenoble, FR, VERIMAG, 2008, s. 36
 Habermehl Peter, Vojnar Tomáš (editors): Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08, Toronto, CA, FIT VUT, 2008, s. 74, ISBN 978-80-214-3697-8

Vaše IPv4 adresa: 184.72.91.94
Přepnout na IPv6 spojení

DNSSEC [dnssec]