Conference paper

ABDULLA Parosh A., HAZIZA Frédéric and HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Berlin: Springer Verlag, 2014, pp. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743. Available from: http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1
Publication language:english
Original title:Block Me If You Can! Context-Sensitive Parameterized Verification
Title (cs):Zablokuj mě jestli můžeš! Prametrická verifikace citlivá na kontext
Pages:1-17
Proceedings:21st International Static Analysis Symposium
Conference:21st International Static Analysis Symposium -- SAS 2014
Series:Lecture Notes in Computer Science
Place:Berlin, DE
Year:2014
URL:http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1
ISBN:978-3-319-10935-0
Journal:Lecture Notes in Computer Science, Vol. 2014, No. 8723, DE
ISSN:0302-9743
Publisher:Springer Verlag
Keywords
parameterized systems
verification
paralelism
concurrency
abstraction
well-quasi ordering
Annotation
We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
Abstract
We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
BibTeX:
@INPROCEEDINGS{
   author = {A. Parosh Abdulla and Fr{\'{e}}d{\'{e}}ric Haziza and
	Luk{\'{a}}{\v{s}} Hol{\'{i}}k},
   title = {Block Me If You Can! Context-Sensitive Parameterized
	Verification},
   pages = {1--17},
   booktitle = {21st International Static Analysis Symposium},
   series = {Lecture Notes in Computer Science},
   journal = {Lecture Notes in Computer Science},
   volume = {2014},
   number = {8723},
   year = {2014},
   location = {Berlin, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-319-10935-0},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=10698}
}

Your IPv4 address: 54.224.50.28
Switch to IPv6 connection

DNSSEC [dnssec]