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: Standardní projekty

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) – hlavní řešitel
Publikace

2012

  • HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. FORMAL METHODS IN SYSTEM DESIGN, 2012, vol. 2012, no. 41, p. 83-106. ISSN: 0925-9856. Detail
  • ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.; BOUAJJANI, A. Abstract Regular (Tree) Model Checking. International Journal on Software Tools for Technology Transfer, 2012, vol. 14, no. 2, p. 167-191. ISSN: 1433-2779. Detail

2011

  • HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6806, p. 424-440. ISSN: 0302-9743. Detail

2010

  • HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. Computing and Informatics, 2010, vol. 2010, no. 7, p. 1337-1348. ISSN: 1335-9150. Detail

2009

  • HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009. p. 93-101. ISBN: 978-3-939897-15-6. Detail
  • IOSIF, R.; ROGALEWICZ, A. Automata-Based Termination Proofs. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 165-177. ISBN: 978-3-642-02978-3. Detail
Nahoru