Project detail

Developement of techniques for automatic verification of programs with dynamic data structures

Duration: 01.01.2009 — 31.12.2011

Funding resources

Czech Science Foundation - Standardní projekty

- whole funder (2009-01-01 - 2011-12-31)

On the project

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.

Description in English
Use of the dynamic data structures is a common technique used in all bigger software systems. On the other hand, searching for errors in such systems is very complicated thanks to the fact that the data structure itself is hidden behind the tricky pointer manipulations. Hence the automated methods for such programs are greatly welcome. The whole verification problem is much more complicated in the case, where several concurrent processes use a shared memory. Bad interference of one of these processes into a dynamic data structure inside the shared memory can interferes the other processes. Another complication for the verification is recursive functions calls. Despite of the huge progress in this area, a reliable verification tool for common use is still far away. Therefore the goal of the proposed basic research project is development of methods for this class of programs.

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

Key words in English
formal verification, model checking, infinite state-space systems, dynamic data structures

Mark

GP201/09/P531

Default language

Czech

People responsible

Rogalewicz Adam, doc. Mgr., Ph.D. - principal person responsible

Units

Faculty of Information Technology
- beneficiary (2009-01-01 - 2011-12-31)

Results

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

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.; 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

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno: 2009. p. 0-0.
Detail

HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno: 2009. p. 0-0.
Detail

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. p. 0-0.
Detail

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

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

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

ŠIMÁČEK, J.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; HABERMEHL, P.: fapointers; Forester: A Tool for Verification of Programs with Pointers. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/forester/. URL: https://www.fit.vut.cz/research/product/142/. (software)
Detail

LENGÁL, O.; HOLÍK, L.; VOJNAR, T.: libSFTA; libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype. https://github.com/ondrik/libsfta. URL: https://github.com/ondrik/libsfta. (software)
Detail

ŠIMÁČEK, J.; HOLÍK, L.; VOJNAR, T.: SA; Tool for Computing Simulations. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/sa/. URL: https://www.fit.vut.cz/research/product/131/. (software)
Detail

Responsibility: Rogalewicz Adam, doc. Mgr., Ph.D.