Detail publikace

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

ROGALEWICZ, A.

Originální název

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

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

ROGALEWICZ, A.

Rok RIV

2006

Vydáno

1. 11. 2006

Nakladatel

Faculty of Information Technology BUT

Místo

Brno

ISBN

80-214-3287-X

Kniha

Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science

Strany od

198

Strany do

205

Strany počet

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