Publication result 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

Peer-reviewed article not indexed in WoS or Scopus

Original Abstract

The paper deals with the problem of automatic verification of programsworking with extended linear linked dynamic data structures, inparticular, pattern-based verification is considered. In this approach,one can abstract memory configurations by abstracting away the exactnumber of adjacent occurrences of certain memory patterns. With respectto the previous work on the subject the method presented in the paperhas been extended to be able to handle multiple patterns, which allowsfor verification of programs working with more types of structuresand/or with structures with irregular shapes. The experimental resultsobtained from a prototype implementation of the method show that themethod is very competitive and offers a big potential for futureextensions.

English abstract

The paper deals with the problem of automatic verification of programsworking with extended linear linked dynamic data structures, inparticular, pattern-based verification is considered. In this approach,one can abstract memory configurations by abstracting away the exactnumber of adjacent occurrences of certain memory patterns. With respectto the previous work on the subject the method presented in the paperhas been extended to be able to handle multiple patterns, which allowsfor verification of programs working with more types of structuresand/or with structures with irregular shapes. The experimental resultsobtained from a prototype implementation of the method show that themethod is very competitive and offers a big potential for futureextensions.

Keywords

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

Key words in English

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

Authors

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

Released

30.03.2007

ISBN

0934-5043

Periodical

FORMAL ASPECTS OF COMPUTING

Volume

19

Number

3

State

United States of America

Pages from

363

Pages to

374

Pages count

12

URL

http://www.springerlink.com/content/47472236k6213t7l/

Full text in the Digital Library

http://hdl.handle.net/

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",
  journal="FORMAL ASPECTS OF COMPUTING",
  year="2007",
  volume="19",
  number="3",
  pages="363--374",
  issn="0934-5043",
  url="http://www.springerlink.com/content/47472236k6213t7l/"
}