%0 Conference Paper %1 Clarke06environmentabstraction %A Clarke, Edmund %A Talupur, Muralidhar %A Veith, Helmut %B In 7 th VMCAI, LNCS 3855 %D 2006 %I Springer %K abstraction modelchecking parameterized reduction verification %P 126--141 %T Environment abstraction for parameterized verification %U http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.89.5154 %X Abstract. Many aspects of computer systems are naturally modeled as parameterized systems which renders their automatic verification difficult. In wellknown examples such as cache coherence protocols and mutual exclusion protocols, the unbounded parameter is the number of concurrent processes which run the same distributed algorithm. In this paper, we introduce environment abstraction as a tool for the verification of such concurrent parameterized systems. Environment abstraction enriches predicate abstraction by ideas from counter abstraction; it enables us to reduce concurrent parameterized systems with unbounded variables to precise abstract finite state transition systems which can be verified by a finite state model checker. We demonstrate the feasibility of our approach by verifying the safety and liveness properties of Lamport’s bakery algorithm and Szymanski’s mutual exclusion algorithm. To the best of our knowledge, this is the first time both safety and liveness properties of the bakery algorithm have been verified at this level of automation. 1

@inproceedings{Clarke06environmentabstraction, abstract = {Abstract. Many aspects of computer systems are naturally modeled as parameterized systems which renders their automatic verification difficult. In wellknown examples such as cache coherence protocols and mutual exclusion protocols, the unbounded parameter is the number of concurrent processes which run the same distributed algorithm. In this paper, we introduce environment abstraction as a tool for the verification of such concurrent parameterized systems. Environment abstraction enriches predicate abstraction by ideas from counter abstraction; it enables us to reduce concurrent parameterized systems with unbounded variables to precise abstract finite state transition systems which can be verified by a finite state model checker. We demonstrate the feasibility of our approach by verifying the safety and liveness properties of Lamport’s bakery algorithm and Szymanski’s mutual exclusion algorithm. To the best of our knowledge, this is the first time both safety and liveness properties of the bakery algorithm have been verified at this level of automation. 1}, added-at = {2010-01-06T17:26:01.000+0100}, author = {Clarke, Edmund and Talupur, Muralidhar and Veith, Helmut}, biburl = {https://www.bibsonomy.org/bibtex/2bb0f2f072d98ab8244f3288c5a481f6d/giuliano.losa}, booktitle = {In 7 th VMCAI, LNCS 3855}, description = {Environment abstraction for parameterized verification}, interhash = {9f1c9ee79bf7104cca80a5def74f5cb7}, intrahash = {bb0f2f072d98ab8244f3288c5a481f6d}, keywords = {abstraction modelchecking parameterized reduction verification}, pages = {126--141}, publisher = {Springer}, timestamp = {2010-01-06T17:43:44.000+0100}, title = {Environment abstraction for parameterized verification}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.89.5154}, year = 2006 }