Project Details

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

Project Period: 1. 1. 2009 - 31. 12. 2011

Project Type: grant

Code: GP201/09/P531

Agency: Czech Science Foundation

Program: Postdoktorandské granty

English title
Developement of techniques for automatic verification of programs with dynamic data structures
Type
grant
Keywords

formal verification, model checking, infinite state-space systems, dynamic data structures

Abstract

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.

Team members
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT) , research leader
Publications

2012

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

2011

  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. Lecture Notes in Computer Science, vol. 2011, no. 6806, pp. 424-440. ISSN 0302-9743. Detail
  • HABERMEHL Peter, HOLÍK Lukáš, ROGALEWICZ Adam, ŠIMÁČEK Jiří and VOJNAR Tomáš. Forest Automata for Verification of Heap Manipulation. FIT-TR-2011-01, Brno: Faculty of Information Technology BUT, 2011. Detail

2010

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

2009

  • IOSIF Radu and ROGALEWICZ Adam. Automata-Based Termination Proofs. In: Implementation and Application of Automata. Lecture Notes in Computer Science, vol. 5642. Berlin: Springer Verlag, 2009, pp. 165-177. ISBN 978-3-642-02978-3. Detail
  • ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang and VOJNAR Tomáš. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno, 2009. Detail
  • HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno, 2009. Detail
  • HOLÍK Lukáš and ŠIMÁČEK Jiří. Optimizing an LTS-Simulation Algorithm. In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009, pp. 93-101. ISBN 978-3-939897-15-6. Detail
Products

2010

  • Forester: A Tool for Verification of Programs with Pointers, software, 2010
    Authors: Habermehl Peter, Holík Lukáš, Rogalewicz Adam, Šimáček Jiří, Vojnar Tomáš Detail
  • libSFTA: A Semi-symbolic Nondeterministic Finite Tree Automata Library Prototype, software, 2010
    Authors: Holík Lukáš, Lengál Ondřej, Vojnar Tomáš Detail

2009

  • Tool for Computing Simulations, software, 2009
    Authors: Holík Lukáš, Šimáček Jiří, Vojnar Tomáš Detail
Back to top