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) – 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. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011. Detail
  • 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
  • HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno: 2009. Detail
  • HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno: 2009. 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
Produkty

2010

2009

Nahoru