Publication Details

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

ROGALEWICZ, A. Abstract Regular Model Checking of Complex Dynamic Data Structures - Implementation Details. Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Information Technology BUT, 2006. p. 198-205. ISBN: 80-214-3287-X.
Czech title
Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu - Implementační detaily
Type
conference paper
Language
English
Authors
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
URL
Keywords

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

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.

Published
2006
Pages
198–205
Proceedings
Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
ISBN
80-214-3287-X
Publisher
Faculty of Information Technology BUT
Place
Brno
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"
}
Back to top