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

English Title

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

Type

Paper in proceedings outside WoS and Scopus

Original Abstract

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

English abstract

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

Keywords

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

Key words in English

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

Authors

ROGALEWICZ, A.

Released

01.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

URL

http://www.fit.vutbr.cz/~rogalew/pubs/artmc_impl.pdf

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",
  url="http://www.fit.vutbr.cz/~rogalew/pubs/artmc_impl.pdf"
}