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: Standardní projekty

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