Block me if you can!: Context-sensitive parameterized verification
2014 (English)In: Static Analysis: SAS 2014, Springer, 2014, 1-17 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Springer, 2014. 1-17 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8723
IdentifiersURN: urn:nbn:se:uu:diva-260087DOI: 10.1007/978-3-319-10936-7_1ISI: 000360204700001ISBN: 978-3-319-10935-0OAI: oai:DiVA.org:uu-260087DiVA: diva2:846306
21st International Symposium, SAS 2014, September 11–13, Munich, Germany