Detail publikace

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

ERLEBACH, P.

Originální název

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

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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. 

Klíčová slova

pattern-based verification, infinite state space, abstraction

Autoři

ERLEBACH, P.

Rok RIV

2005

Vydáno

14. 10. 2005

Nakladatel

Faculty of Informatics MU

Místo

Brno

Strany od

145

Strany do

154

Strany počet

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"
}