environment abstraction with state clustering and parameter truncating

	environment abstraction with state clustering and parameter truncating
	Pan Hong; Lv Yi; Lin Huimin
	2009
会议名称	3rd International Symposium on Theoretical Aspects of Software Engineering
会议录名称	Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009
会议日期	JUL 29-31,
会议地点	Tianjin, PEOPLES R CHINA
出版地	10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA
出版者	THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS
ISBN	978-0-7695-3757-3
部门归属	Pan, Hong; Lv, Yi; Lin, Huimin Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing 100190, Peoples R China.
摘要	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.
关键词	Computer Software Model Checking
主办者	IEEE Comp Soc, IFIP, Tianjin Normal Univ
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/8304
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	Pan Hong,Lv Yi,Lin Huimin. environment abstraction with state clustering and parameter truncating[C]. 10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA:THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS,2009.