Faculty of Information Technology, BUT

Publication Details

Block Me If You Can! Context-Sensitive Parameterized Verification

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. Lecture Notes in Computer Science, vol. 2014. 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
Czech title
Zablokuj mě jestli můžeš! Prametrická verifikace citlivá na kontext
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Haziza Frédéric (Uppsala)
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
URL
Keywords
parameterized systems
verification
paralelism
concurrency
abstraction
well-quasi ordering
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.
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.
Published
2014
Pages
1-17
Journal
Lecture Notes in Computer Science, vol. 2014, no. 8723, ISSN 0302-9743
Proceedings
21st International Static Analysis Symposium
Series
Lecture Notes in Computer Science
Conference
21st International Static Analysis Symposium -- SAS 2014, Mnichov, DE
ISBN
978-3-319-10935-0
Publisher
Springer Verlag
Place
Berlin, DE
DOI
BibTeX
@INPROCEEDINGS{FITPUB10698,
   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",
   doi = "10.1007/978-3-319-10936-7\_1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10698"
}
Back to top