Detail publikace

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata

Originální název

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata

Anglický název

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata

Jazyk

en

Originální abstrakt

We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. Our framework is based on the notion of forest automata (FA) previously developed for verification of heap-manipulating programs. We extend FA by constraints between data elements associated with nodes of the heaps represented by FA, and we propose necessary modifications of all the operations needed for a use of the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool, and applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists. The experiments show that our approach is not only fully automated, rather general, but also quite efficient.

Anglický abstrakt

We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. Our framework is based on the notion of forest automata (FA) previously developed for verification of heap-manipulating programs. We extend FA by constraints between data elements associated with nodes of the heaps represented by FA, and we propose necessary modifications of all the operations needed for a use of the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool, and applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists. The experiments show that our approach is not only fully automated, rather general, but also quite efficient.

BibTex


@inproceedings{BUT103527,
  author="Lukáš {Holík} and Bengt {Jonsson} and Ondřej {Lengál} and Tomáš {Vojnar} and Quy Cong {Trinh} and Parosh {Abdulla}",
  title="Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata",
  annote="We present a general framework for verifying programs with complex dynamic linked
data structures whose correctness depends on ordering relations between stored
data values. Our framework is based on the notion of forest automata (FA)
previously developed for verification of heap-manipulating programs. We extend FA
by constraints between data elements associated with nodes of the heaps
represented by FA, and we propose necessary modifications of all the operations
needed for a use of the extended FA in a fully-automated verification approach,
based on abstract interpretation. We have implemented our approach as an
extension of the Forester tool, and applied it to a number of programs dealing
with data structures such as various forms of singly- and doubly-linked lists,
binary search trees, as well as skip lists. The experiments show that our
approach is not only fully automated, rather general, but also quite efficient.",
  address="Springer Verlag",
  booktitle="Proceedings of ATVA'13",
  chapter="103527",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Springer Verlag",
  year="2013",
  month="october",
  pages="224--239",
  publisher="Springer Verlag",
  type="conference paper"
}