About: All for the Price of Few (Parameterized Verification through View Abstraction)

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

About: All for the Price of Few (Parameterized Verification through View Abstraction) 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 present a simple and efficient framework for automatic verification of systems with parameteric number of communicating processes. The processes may be organized in various topologies such words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large subclass of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problem. We present a simple and efficient framework for automatic verification of systems with parameteric number of communicating processes. The processes may be organized in various topologies such words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large subclass of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problem. (en)
Title	All for the Price of Few (Parameterized Verification through View Abstraction) All for the Price of Few (Parameterized Verification through View Abstraction) (en)
skos:prefLabel	All for the Price of Few (Parameterized Verification through View Abstraction) All for the Price of Few (Parameterized Verification through View Abstraction) (en)
skos:notation	RIV/00216305:26230/13:PU106293!RIV14-GA0-26230___
http://linked.open...avai/predkladatel	Fakulta informačních technologií
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(GAP103/10/0306)
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Holík, Lukáš
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	60116
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/13:PU106293
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	parameterized verification, communication protocols, well-quasi ordered systems, abstraction, cutoff (en)
http://linked.open.../riv/klicoveSlovo	cutoff parameterized verification well-quasi ordered systems abstraction communication protocols
http://linked.open...ontrolniKodProRIV	[5AE981F8329A]
http://linked.open...v/mistoKonaniAkce	Řím
http://linked.open...i/riv/mistoVydani	Berlin Heidelberg
http://linked.open...i/riv/nazevZdroje	Proc. of VMCAI 2013
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
http://linked.open...UplatneniVysledku	2013
http://linked.open...iv/tvurceVysledku	Abdulla, Parosh Holík, Lukáš Haziza, Frédéric
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2013-01-20 (xsd:date)
number of pages	20 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-642-35872-2
http://localhost/t...ganizacniJednotka	26230

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