Result 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.
Type
conference paper
Language
English
Authors
Rogalewicz Adam, doc. Mgr., Ph.D., DITS (FIT)
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.
URL
Published
2006
Pages
198–205
Proceedings
Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Conference
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science -- MEMICS'06
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"
}
Projects
Integrated approach to education of PhD students in the area of parallel and distributed systems, GACR, Doktorské granty, GD102/05/H050, start: 2005-01-01, end: 2008-12-31, completed
Research groups
Departments