Detail publikace

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

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

Originální název

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

Typ

článek v časopise - ostatní, Jost

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Rok RIV

2007

Vydáno

30. 3. 2007

ISSN

0934-5043

Periodikum

Formal Aspects of Computing

Ročník

19

Číslo

3

Stát

Spojené státy americké

Strany od

363

Strany do

374

Strany počet

12

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