About: Programs with Lists are Counter Automata

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Programs with Lists are Counter Automata Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	We address the problem of verifying programs manipulating one-selector linked data structures. We propose and study in detail an application of counter automata as an accurate abstract model for this problem. We let control states of the counter automata correspond to abstract heap graphs where list segments without sharing are collapsed, and use counters to keep track of the number of elements in these segments. As a significant theoretical result, we show that the obtained counter automata are bisimilar to the original programs. Moreover, from a practical point of view, our translation allows one to apply efficient automatic analysis techniques and tools developed for counter automata (integer programs) in order to verify both safety as well as termination of list-manipulating programs. As another theoretical contribution, we prove that if the control of the generated counter automata does not contain nested loops (i.e., these automata are flat), both safety and termination are decidable We address the problem of verifying programs manipulating one-selector linked data structures. We propose and study in detail an application of counter automata as an accurate abstract model for this problem. We let control states of the counter automata correspond to abstract heap graphs where list segments without sharing are collapsed, and use counters to keep track of the number of elements in these segments. As a significant theoretical result, we show that the obtained counter automata are bisimilar to the original programs. Moreover, from a practical point of view, our translation allows one to apply efficient automatic analysis techniques and tools developed for counter automata (integer programs) in order to verify both safety as well as termination of list-manipulating programs. As another theoretical contribution, we prove that if the control of the generated counter automata does not contain nested loops (i.e., these automata are flat), both safety and termination are decidable (en)
Title	Programs with Lists are Counter Automata Programs with Lists are Counter Automata (en)
skos:prefLabel	Programs with Lists are Counter Automata Programs with Lists are Counter Automata (en)
skos:notation	RIV/00216305:26230/11:PU96018!RIV13-MSM-26230___
http://linked.open...avai/predkladatel	Fakulta informačních technologií
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(GAP103/10/0306), P(OC10009), S, Z(MSM0021630528)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2013
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	224452
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/11:PU96018
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	formal verification, model checking, programs with linked lists, counter automata, bisimulation (en)
http://linked.open.../riv/klicoveSlovo	model checking formal verification bisimulation counter automata programs with linked lists
http://linked.open...odStatuVydavatele	US - Spojené státy americké
http://linked.open...ontrolniKodProRIV	[5018A1E82F35]
http://linked.open...i/riv/nazevZdroje	FORMAL METHODS IN SYSTEM DESIGN
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	6 (xsd:int)
http://linked.open...vavai/riv/projekt	Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
http://linked.open...UplatneniVysledku	2011
http://linked.open...v/svazekPeriodika	38
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Habermehl, Peter Bouajjani, Ahmed Bozga, Marius Moro, Pierre Radu, Iosif
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
issn	0925-9856
number of pages	35 (xsd:int)
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Programs with Lists are Counter Automata

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software