Detail výsledku
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
Článek představuje metodu pro automatickou verifikaci systémů s parametrickým počtem komunikujících procesů, jako jsou protokoly pro vzájemné vyloučení. Za tímto účelem jsme navrhli efektivní a přesnou abstrakci. Metoda je obecnější než metody specializující se na dobře quasi-uspořádané systémy. Experimentálně jsme ověřili její efektivitu. Byli jsme schopni zverifikovat některé systémy, které dříve nebyly automaticky verifikovány, jako například plná verze Szymanského algoritmu pro vzájemné vyloučení.
@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, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Verifikace nekonečně stavových systémů založená na konečných automatech, GAČR, Postdoktorandské granty, GP13-37876P, zahájení: 2013-02-01, ukončení: 2015-12-31, ukončen