Publication result detail

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

ERLEBACH, P.

Original Title

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

English Title

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

Type

Paper in proceedings outside WoS and Scopus

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

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

Keywords

pattern-based verification, infinite state space, abstraction

Key words in English

pattern-based verification, infinite state space, abstraction

Authors

ERLEBACH, P.

Released

14.10.2005

Publisher

Faculty of Informatics MU

Location

Brno

Book

PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science

Pages from

145

Pages to

154

Pages count

10

BibTex

@inproceedings{BUT18289,
  author="Pavel {Erlebach}",
  title="Towards a Systematic Framework for Automatic Pattern-Based Verification of Dynamic Data Structures",
  booktitle="PRE-PROCEEDINGS of the 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science",
  year="2005",
  pages="145--154",
  publisher="Faculty of Informatics MU",
  address="Brno",
  isbn="0"
}