Publication detail

Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures

ERLEBACH, P. ČEŠKA, M. VOJNAR, T.

Original Title

Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures

English Title

Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures

Type

journal article - other

Language

en

Original Abstract

The paper deals with the problem of automatic verification of programs working with extended linear linked dynamic data structures, in particular, pattern-based verification is considered. In this approach, one can abstract memory configurations by abstracting away the exact number of adjacent occurrences of certain memory patterns. With respect to the previous work on the subject the method presented in the paper has been extended to be able to handle multiple patterns, which allows for verification of programs working with more types of structures and/or with structures with irregular shapes. The experimental results obtained from a prototype implementation of the method show that the method is very competitive and offers a big potential for future extensions.

English abstract

The paper deals with the problem of automatic verification of programs working with extended linear linked dynamic data structures, in particular, pattern-based verification is considered. In this approach, one can abstract memory configurations by abstracting away the exact number of adjacent occurrences of certain memory patterns. With respect to the previous work on the subject the method presented in the paper has been extended to be able to handle multiple patterns, which allows for verification of programs working with more types of structures and/or with structures with irregular shapes. The experimental results obtained from a prototype implementation of the method show that the method is very competitive and offers a big potential for future extensions.

Keywords

formal verification, program analysis, shape analysis, dynamic linked data structures

RIV year

2007

Released

30.03.2007

ISBN

0934-5043

Periodical

Formal Aspects of Computing

Year of study

19

Number

3

State

US

Pages from

363

Pages to

374

Pages count

12

Documents

BibTex 


@article{BUT45155,
  author="Pavel {Erlebach} and Milan {Češka} and Tomáš {Vojnar}",
  title="Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures",
  annote="The paper deals with the problem of automatic verification of programs working
with extended linear linked dynamic data structures, in particular, pattern-based
verification is considered. In this approach, one can abstract memory
configurations by abstracting away the exact number of adjacent occurrences of
certain memory patterns. With respect to the previous work on the subject the
method presented in the paper has been extended to be able to handle multiple
patterns, which allows for verification of programs working with more types of
structures and/or with structures with irregular shapes. The experimental results
obtained from a prototype implementation of the method show that the method is
very competitive and offers a big potential for future extensions.",
  chapter="45155",
  howpublished="print",
  journal="Formal Aspects of Computing",
  number="3",
  volume="19",
  year="2007",
  month="march",
  pages="363--374",
  type="journal article - other"
}