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. (DITS) – research leader
Publications

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. p. 0-0. 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. p. 0-0. 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
  • 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
Back to top