Block Me If You Can! Context-Sensitive Parameterized Verification

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áš, doc. Mgr., Ph.D. (DITS FIT BUT)

URL

http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1

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

10.1007/978-3-319-10936-7_1

UT WoS

000360204700001

EID Scopus

2-s2.0-84921744929

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"
}