Detail publikačního výsledku

Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools

ERLEBACH, P.; VOJNAR, T.

Originální název

Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools

Anglický název

Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

This paper investigates capabilities of two advanced state-of-the-art tools-namely Pale and TVLA-for automated formal verification of programs manipulating unbounded dynamic data structures. We consider verification of operations dealing with binary search trees over which we want to verify the basic correctness of pointer manipulations (no null pointer dereferences, etc.) as well as the sortedness requirement of binary search trees. Unlike in other works, we want to verify the full sortedness requirement, i.e. that all nodes in the left subtree of a node n are smaller than n, and all nodes in the right subtree of n are bigger than n (and not just the relation between a node and its direct subnodes). For the needs of verifying this property in the TVLA tool, we provide a new kind of instrumentation predicate that allows one to handle such a property.

Anglický abstrakt

This paper investigates capabilities of two advanced state-of-the-art tools-namely Pale and TVLA-for automated formal verification of programs manipulating unbounded dynamic data structures. We consider verification of operations dealing with binary search trees over which we want to verify the basic correctness of pointer manipulations (no null pointer dereferences, etc.) as well as the sortedness requirement of binary search trees. Unlike in other works, we want to verify the full sortedness requirement, i.e. that all nodes in the left subtree of a node n are smaller than n, and all nodes in the right subtree of n are bigger than n (and not just the relation between a node and its direct subnodes). For the needs of verifying this property in the TVLA tool, we provide a new kind of instrumentation predicate that allows one to handle such a property.

Klíčová slova

automated formal verification, TVLA, PALE, full sortedness, insertBST

Klíčová slova v angličtině

automated formal verification, TVLA, PALE, full sortedness, insertBST

Autoři

ERLEBACH, P.; VOJNAR, T.

Vydáno

19.04.2005

Nakladatel

Marq software s.r.o.

Místo

Ostrava

ISBN

80-86840-09-3

Kniha

Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling

Strany od

219

Strany do

226

Strany počet

8

BibTex

@inproceedings{BUT21471,
  author="Pavel {Erlebach} and Tomáš {Vojnar}",
  title="Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools",
  booktitle="Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling",
  year="2005",
  pages="219--226",
  publisher="Marq software s.r.o.",
  address="Ostrava",
  isbn="80-86840-09-3"
}