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 be yond 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.

作者: Hong Pan Yi Lv Huimin Lin

作者单位: State Key Laboratory of Computer Science, Institute of Software Chinese Academy of Sciences P.O.Box 8718, Beijing 100190, China

会议类型: 国际会议

会议名称: Third International Symposium on Theoretical Aspects of Software Engineering TASE 2009(第三届软件工程理论国际研讨会)

会议地点: 天津

会议语种:英文

页码: 73-80

在线出版日期: 2009-07-29（万方平台首次上网日期，不代表论文的发表时间）