Publication detail

Abstract Regular Model Checking of Complex Dynamic Data Structures - Implementation Details

ROGALEWICZ, A.

Original Title

Abstract Regular Model Checking of Complex Dynamic Data Structures - Implementation Details

Type

conference paper

Language

English

Original Abstract

This article describes some implementation details used in our prototype tool for verification of programs manipulating dynamic data structures. This tool is based on the automata framework. We encode data structures into trees and sets of trees as finite tree automata. The program behaviour is encoded as a tree transducer. Then the abstract regular tree model checking technique can be applied to compute a set of all reachable configurations.

Keywords

Formal verification, symbolic verification, shape analysis, dynamic data structures, tree automata.

Authors

ROGALEWICZ, A.

RIV year

2006

Released

1. 11. 2006

Publisher

Faculty of Information Technology BUT

Location

Brno

ISBN

80-214-3287-X

Book

Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science

Pages from

198

Pages to

205

Pages count

8

BibTex

@inproceedings{BUT22279,
  author="Adam {Rogalewicz}",
  title="Abstract Regular Model Checking of Complex Dynamic Data Structures - Implementation Details",
  booktitle="Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science",
  year="2006",
  pages="198--205",
  publisher="Faculty of Information Technology BUT",
  address="Brno",
  isbn="80-214-3287-X"
}