Programs with Lists are Counter Automata

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Programs with Lists are Counter Automata

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Programs with Lists are Counter Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GA102%2F04%2F0780" target="_blank" >GA102/04/0780: Automatizované metody a nástroje pro vývoj spolehlivých paralelních a distribuovaných systémů</a><br>

Návaznosti

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

Rok uplatnění

2006

Kód důvěrnosti údajů

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

Název statě ve sborníku

Computer Aided Verification

ISBN

978-3-540-37406-0

ISSN

—

e-ISSN

—

Počet stran výsledku

15

Strana od-do

—

Název nakladatele

Springer Verlag

Místo vydání

Berlin

Místo konání akce

Seattle, Washington

Datum konání akce

12. 5. 2006

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—