Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
ABDULLA, P. HAZIZA, F. HOLÍK, L.
Originální název
Block Me If You Can! Context-Sensitive Parameterized Verification
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
parameterized systems verification paralelism concurrency abstraction well-quasi ordering
Autoři
ABDULLA, P.; HAZIZA, F.; HOLÍK, L.
Rok RIV
2014
Vydáno
11. 11. 2014
Nakladatel
Springer Verlag
Místo
Berlin
ISBN
978-3-319-10935-0
Kniha
21st International Static Analysis Symposium
Edice
Lecture Notes in Computer Science
ISSN
0302-9743
Periodikum
Ročník
Číslo
8723
Stát
Spolková republika Německo
Strany od
1
Strany do
17
Strany počet
URL
http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1
BibTex
@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" }