Result Details
Block Me If You Can! Context-Sensitive Parameterized Verification
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.
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.
@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"
}Spolehlivost a bezpečnost v IT, BUT, Vnitřní projekty VUT, FIT-S-14-2486, start: 2014-01-01, end: 2016-12-31, completed
Verification of Infinite State Systems Based on Finite Automata, GACR, Postdoktorandské granty, GP13-37876P, start: 2013-02-01, end: 2015-12-31, completed
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed