About: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

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

About: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking 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 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, abstract regular 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 introduce new techniques 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, abstract regular 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 introduce new techniques (en)
Title	Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking (en)
skos:prefLabel	Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking (en)
skos:notation	RIV/00216305:26230/05:PU56426!RIV10-GA0-26230___
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(GA102/04/0780), P(GP102/03/D211)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
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	548724
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/05:PU56426
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	formal verification, model checking, infinite-state systems, software verification, dynamic data structures<br> (en)
http://linked.open.../riv/klicoveSlovo	dynamic data structures<br> software verification model checking formal verification infinite-state systems
http://linked.open...ontrolniKodProRIV	[BFDBEAE2C889]
http://linked.open...v/mistoKonaniAkce	Edinburgh
http://linked.open...i/riv/mistoVydani	Berlin
http://linked.open...i/riv/nazevZdroje	Tools and Algorithms for the Construction and Analysis of Systems
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	4 (xsd:int)
http://linked.open...vavai/riv/projekt	Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems Automated methods and tools supporting development of reliable concurrent and distributed systems
http://linked.open...UplatneniVysledku	2005
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Habermehl, Peter Bouajjani, Ahmed Moro, Pierre
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2005-04-02 (xsd:date)
number of pages	17 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-540-25333-4
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking

Faceted Search & Find service v1.16.116 as of Feb 22 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

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