Detail projektu

Techniques avancées pour la vérification de systémes a nombre d'états infini

Období řešení: 20. 2. 2008 - 31. 12. 2009

Typ projektu: grant

Kód: MEB 020840

Agentura: Barrande - česko-francouzský program integrovaných akcí

Program:

Typ
grant
Klíčová slova

formální verifikace, nekonečně stavové systémy, model checking

Abstrakt

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.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Habermehl Peter (UPAR7) , spoluřešitel
Bouajjani Ahmed (UPAR7)
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Touili Tayssir (LIAFA UP7/CNRS)
Publikace

2010

  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Acta Informatica, roč. 47, č. 1, 2010, s. 1-31. ISSN 0001-5903. Detail

2009

  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. Electronic Notes in Theoretical Computer Science, roč. 2009, č. 251, s. 27-48. ISSN 1571-0661. Detail
  • IOSIF Radu a ROGALEWICZ Adam. Automata-Based Termination Proofs. In: Implementation and Application of Automata. Lecture Notes in Computer Science, roč. 5642. Berlin: Springer Verlag, 2009, s. 165-177. ISBN 978-3-642-02978-3. Detail
  • BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip a VOJNAR Tomáš. Automatic Verification of Integer Array Programs. In: Computer Aided Verification. Lecture Notes in Computer Science, roč. 5643. Berlin: Springer Verlag, 2009, s. 157-172. ISBN 978-3-642-02657-7. Detail
  • BOZGA Marius, HABERMEHL Peter, IOSIF Radu, KONEČNÝ Filip a VOJNAR Tomáš. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Composed Bisimulation for Tree Automata. International Journal of Foundations of Computer Science, roč. 20, č. 4, 2009, s. 685-700. ISSN 0129-0541. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Fakulta informačních technologií VUT v Brně, 2009. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno, 2009. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang a 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). LIPIcs, sv. 4. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009, s. 1-12. ISBN 978-3-939897-13-2. Detail
  • HOLÍK Lukáš a ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno, 2009. Detail
  • HOLÍK Lukáš a ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Fakulta informatiky MU, 2009, s. 93-101. ISBN 978-3-939897-15-6. Detail

2008

  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. A Logic of Singly Indexed Arrays. In: Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science, roč. 5330. Berlin: Springer Verlag, 2008, s. 558-573. ISBN 978-3-540-89438-4. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, KAATI Lisa a 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: Fakulta informatiky MU, 2008, s. 3-11. ISBN 978-80-7355-082-0. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir a VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. In: Implementation and Application of Automata. Lecture Notes in Computer Science, roč. 5148. Berlin: Springer Verlag, 2008, s. 57-67. ISBN 978-3-540-70843-8. Detail
  • BOUAJJANI Ahmed, HABERMEHL Peter, HOLÍK Lukáš, TOUILI Tayssir a VOJNAR Tomáš. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Fakulta informačních technologií VUT v Brně, 2008. Detail
  • ABDULLA Parosh A., BOUAJJANI Ahmed, HOLÍK Lukáš, KAATI Lisa a VOJNAR Tomáš. Composed Bisimulation for Tree Automata. In: Implementation and Application of Automata. Lecture Notes in Computer Science, roč. 5148. Berlin: Springer Verlag, 2008, s. 212-222. ISBN 978-3-540-70843-8. Detail
  • HABERMEHL Peter a VOJNAR Tomáš, ed. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Fakulta informačních technologií VUT v Brně, 2008. ISBN 978-80-214-3697-8. Detail
  • HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008. Detail
Produkty

2009

  • FLATA, software, 2009
    Autoři: Konečný Filip, Vojnar Tomáš, Bozga Marius, Iosif Radu Detail
Nahoru