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

Publikační výsledky

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

Aplikované výsledky

2010

Forester: A Tool for Verification of Programs with Pointers, software, 2010
Autoři: ŠIMÁČEK, J.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.
libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software, 2010
Autoři: LENGÁL, O.; HOLÍK, L.; VOJNAR, T.

2009

Tool for Computing Simulations, software, 2009
Autoři: ŠIMÁČEK, J.; HOLÍK, L.; VOJNAR, T.

Ostatní výsledky

2011

Forest Automata for Verification of Heap Manipulation, zpráva odborná, 2011
Autoři: HOLÍK, L.; ROGALEWICZ, A.; ŠIMÁČEK, J.; VOJNAR, T.; HABERMEHL, P.

2009

Mediating for Reduction (On Minimizing Alternating Büchi Automata), zpráva odborná, 2009
Autoři: HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.
Optimizing an LTS-Simulation Algorithm, zpráva odborná, 2009
Autoři: HOLÍK, L.; ŠIMÁČEK, J.