Detail publikace

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

HOLÍK, L. ABDULLA, P. HAZIZA, F.

Originální název

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

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

parameterized verification, communication protocols, well-quasi ordered systems, abstraction, cutoff

Autoři

HOLÍK, L.; ABDULLA, P.; HAZIZA, F.

Rok RIV

2013

Vydáno

21. 1. 2013

Nakladatel

Springer Verlag

Místo

Berlin Heidelberg

ISBN

978-3-642-35872-2

Kniha

Proc. of VMCAI 2013

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

2013

Číslo

7737

Stát

Spolková republika Německo

Strany od

476

Strany do

495

Strany počet

20

BibTex

@inproceedings{BUT103433,
  author="Lukáš {Holík} and Parosh {Abdulla} and Frédéric {Haziza}",
  title="All for the Price of Few (Parameterized Verification through View Abstraction)",
  booktitle="Proc. of VMCAI 2013",
  year="2013",
  journal="Lecture Notes in Computer Science",
  volume="2013",
  number="7737",
  pages="476--495",
  publisher="Springer Verlag",
  address="Berlin Heidelberg",
  isbn="978-3-642-35872-2",
  issn="0302-9743"
}