Detail projektu

Rozvoj technik pro automatické verifikace programů s dynamickými datovými strukturami

Období řešení: 1. 1. 2009 - 31. 12. 2011

Typ projektu: grant

Kód: GP201/09/P531

Agentura: Grantová agentura České republiky

Program: Postdoktorandské granty

Název anglicky
Developement of techniques for automatic verification of programs with dynamic data structures
Typ
grant
Klíčová slova

Formální verifikace, model checking, nekonečně stavové systémy, dynamické datové struktury

Abstrakt

Použití dynamických datových struktur je běžnou záležitostí používanou ve všech větších softwarových systémech. Hledání chyb v tomto typu programů je ale velmi komplikované. Vlastní datová struktura je totiž ukrytá za manipulacemi s ukazateli, které mohou být záludné. Proto jsou techniky pro automatické ověřování správnosti těchto programů velmi žádané. Celý problém verifikace se dále komplikuje v případě, že několik souběžných procesů přistupuje ke společné dynamické datové struktuře. Chybný zásah jednoho z nich do takovéto sdílené datové struktury může negativně ovlivnit běh ostatních. Další komplikací pro verifikace takovýchto programů jsou rekurzivní volání funkcí. I přes výrazné pokroky v oblasti verifikace programů s dynamickými datovými strukturami je cesta ke spolehlivému verifikačnímu nástroji určenému k širokému použití ještě dlouhá. Navrhovaný projekt základního výzkumu si proto klade za cíl rozvoj automatických verifikačních metod určených pro tyto programy.

Řešitelé
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Publikace

2012

  • BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, roč. 14, č. 2, 2012, s. 167-191. ISSN 1433-2779. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Formal Methods in System Design, roč. 2012, č. 41, s. 83-106. ISSN 0925-9856. Detail

2011

  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, roč. 2011, č. 6806, s. 424-440. ISSN 0302-9743. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří a VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Fakulta informačních technologií VUT v Brně, 2011. Detail

2010

  • HOLÍK Lukáš a ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. Computing and Informatics, roč. 2010, č. 7, s. 1337-1348. ISSN 1335-9150. Detail

2009

  • 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
  • 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
  • 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
Produkty

2010

  • Forester: Nástroj pro verifikaci programů s ukazateli, software, 2010
    Autoři: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš Detail
  • libSFTA: Prototyp knihovny pro efektivní práci se semi-symbolicky reprezentovanými nedeterministickými stromovými automaty, software, 2010
    Autoři: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš Detail

2009

  • Nástroj pro výpočet simulací, software, 2009
    Autoři: Holík Lukáš, Šimáček Jiří, Vojnar Tomáš Detail
Nahoru