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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F13%3APU106293" target="_blank" >RIV/00216305:26230/13:PU106293 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti</a><br>

Návaznosti

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

Rok uplatnění

2013

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

Proc. of VMCAI 2013

ISBN

978-3-642-35872-2

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

20

Strana od-do

476-495

Název nakladatele

Springer Verlag

Místo vydání

Berlin Heidelberg

Místo konání akce

Řím

Datum konání akce

20. 1. 2013

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

WRD - Celosvětová akce

Kód UT WoS článku

—