Programs with Lists are Counter Automata

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F06%3APU86206" target="_blank" >RIV/00216305:26230/06:PU86206 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Programs with Lists are Counter Automata

Original language description

We address the verification problem of programs manipulating one-selector linked data structures. We propose a new automated approach for checking safety and termination for these programs. Our approach is based on using counter automata as accurate abstract models: control states correspond to abstract heap graphs where list segments without sharing are collapsed, and counters are used to keep track of the number of elements in these segments. This allows to apply automatic analysis techniques and tools for counter automata in order to verify list programs. We show the effectiveness of our approach, in particular by verifying automatically termination of some sorting programs.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GA102%2F04%2F0780" target="_blank" >GA102/04/0780: Automated methods and tools supporting development of reliable concurrent and distributed systems</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2006

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Computer Aided Verification

ISBN

978-3-540-37406-0

ISSN

—

e-ISSN

—

Number of pages

15

Pages from-to

—

Publisher name

Springer Verlag

Place of publication

Berlin

Event location

Seattle, Washington

Event date

May 12, 2006

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—