Faculty of Information Technology, BUT

Publication Details

Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures

ERLEBACH Pavel. Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures. In: PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2005, pp. 145-154.
Czech title
Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures
Type
conference paper
Language
english
Authors
Erlebach Pavel, Ing. (DITS FIT BUT)
Keywords
pattern-based verification, infinite state space, abstraction
Abstract
This paper aims at automatic verification of programs working with possibly unbounded dynamic data structures. Namely, it concentrates on pattern-based verification, which is an automatic verification technique usable in this area. Its abstraction consists in clustering isomorphic subgraphs of the structure into so-called summary nodes. The behaviour of the program is then simulated on created summarized shape graphs, which allows to work with unbounded structures. The technique detects errors like dereference over NULL, memory  leakage etc.

This paper gives a theoretical support to pattern-based verification, i.e. the basic notions and their properties are formalized, their practical value is shown, the class of structures, which pattern-based verification can handle, is specified and at the end of the paper some proofs are shown, which demonstrates usability of this technique. 

Published
2005
Pages
145-154
Proceedings
PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Conference
1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science -- MEMICS 2005, Znojmo, CZ
Publisher
Faculty of Informatics MU
Place
Brno, CZ
BibTeX
@INPROCEEDINGS{FITPUB7979,
   author = "Pavel Erlebach",
   title = "Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures",
   pages = "145--154",
   booktitle = "PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science",
   year = 2005,
   location = "Brno, CZ",
   publisher = "Faculty of Informatics MU",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7979"
}
Back to top