Publication Details
Block Me If You Can! Context-Sensitive Parameterized Verification
parameterized systems verification paralelism concurrency abstraction well-quasi ordering
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.
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.
@inproceedings{BUT111638,
author="Parosh {Abdulla} and Frédéric {Haziza} and Lukáš {Holík}",
title="Block Me If You Can! Context-Sensitive Parameterized Verification",
booktitle="21st International Static Analysis Symposium",
year="2014",
series="Lecture Notes in Computer Science",
journal="Lecture Notes in Computer Science",
volume="2014",
number="8723",
pages="1--17",
publisher="Springer Verlag",
address="Berlin",
doi="10.1007/978-3-319-10936-7\{_}1",
isbn="978-3-319-10935-0",
issn="0302-9743",
url="http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1"
}