Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F05%3APU56426" target="_blank" >RIV/00216305:26230/05:PU56426 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking
Original language description
We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive programs manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory are systematically encoded as words over a suitable finite alphabet, potentially infinite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstractregular model checking techniques are applied in order to automatically check safety properties concerning the shape of the computed configurations or relating the input and output configurations. For this particular purpose, we introduc
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2005
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
978-3-540-25333-4
ISSN
—
e-ISSN
—
Number of pages
17
Pages from-to
—
Publisher name
Springer Verlag
Place of publication
Berlin
Event location
Edinburgh
Event date
Apr 2, 2005
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—