Environment Abstraction with State Clustering and Parameter Truncating

Environment abstraction enriches predicate abstraction by idea from counter abstraction to develop a framework for verification of parameterized systems. However, despite various effects, the constructed abstractions still go beyond the capability of the usual model checkers for many realistic systems. In this paper, a new technique, called state clustering, is proposed to group local states into a small number of clusters, by purely syntactic analysis. The size of array variables in the resulting abstractions are further reduced using parameter abstraction technique. By combining different abstraction techniques, real-life cache coherence protocols such as FLASH have been successfully verified.