Conference paper

ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. All for the Price of Few (Parameterized Verification through View Abstraction). In: Proc. of VMCAI 2013. Berlin Heidelberg: Springer Verlag, 2013, pp. 476-495. ISBN 978-3-642-35872-2. ISSN 0302-9743.
Publication language:english
Original title:All for the Price of Few (Parameterized Verification through View Abstraction)
Title (cs):Vše za cenu měkolika (pohledové abstrakce pro parametrickou verifikaci)
Proceedings:Proc. of VMCAI 2013
Conference:14th International Conference on Verification, Model Checking, and Abstract Interpretation
Place:Berlin Heidelberg, DE
Journal:Lecture Notes in Computer Science, Vol. 2013, No. 7737, DE
Publisher:Springer Verlag
parameterized verification, communication protocols, well-quasi ordered systems, abstraction, cutoff
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.
   author = {A. Parosh Abdulla and Fr{\'{e}}d{\'{e}}ric Haziza
	and Luk{\'{a}}{\v{s}} Hol{\'{i}}k},
   title = {All for the Price of Few (Parameterized
	Verification through View Abstraction)},
   pages = {476--495},
   booktitle = {Proc. of VMCAI 2013},
   journal = {Lecture Notes in Computer Science},
   volume = 2013,
 number = 7737,
   year = 2013,
   location = {Berlin Heidelberg, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-642-35872-2},
   ISSN = {0302-9743},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https