All for the Price of Few (Parameterized Verification through View Abstraction)
The result's identifiers
Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
All for the Price of Few (Parameterized Verification through View Abstraction)
Original language 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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proc. of VMCAI 2013
ISBN
978-3-642-35872-2
ISSN
0302-9743
e-ISSN
—
Number of pages
20
Pages from-to
476-495
Publisher name
Springer Verlag
Place of publication
Berlin Heidelberg
Event location
Řím
Event date
Jan 20, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—