Combining symmetry reduction with generalized symbolic trajectory evaluation

ISCAS OpenIR

	Combining symmetry reduction with generalized symbolic trajectory evaluation
	Li, Yongjian (1); Zeng, Naiju (1); Hung, William N.N. (2); Song, Xiaoyu (3); Li, Y.(lyj238@gmail.com)
	2014
发表期刊	Computer Journal
ISSN	104620
卷号	57 期号:1 页码:115-128
摘要	This paper combines symmetry reduction with generalized symbolic trajectory evaluation (GSTE) to tackle state explosion. The inherent correlation between structure symmetry and property symmetry is formalized as a theorem, which provides the soundness of our symmetry reduction method. We introduce a practical strategy to effectively integrate the symmetry-reduction approach in a hybrid verification environment which combines theorem proving and GSTE. The effectiveness of our method is demonstrated by case studies. © 2013 The Author 2013. Published by Oxford University Press on behalf of The British Computer Society. All rights reserved. For Permissions, please email: journals.permissions@oup.com.; This paper combines symmetry reduction with generalized symbolic trajectory evaluation (GSTE) to tackle state explosion. The inherent correlation between structure symmetry and property symmetry is formalized as a theorem, which provides the soundness of our symmetry reduction method. We introduce a practical strategy to effectively integrate the symmetry-reduction approach in a hybrid verification environment which combines theorem proving and GSTE. The effectiveness of our method is demonstrated by case studies. © 2013 The Author 2013. Published by Oxford University Press on behalf of The British Computer Society. All rights reserved. For Permissions, please email: journals.permissions@oup.com.
收录类别	SCI ; EI
关键词	Generalized Symbolic Trajectory Evaluation Symmetry Reduction Theorem Proving
部门归属	(1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (2) Synopsys Inc., Mountain View, CA, United States; (3) Department of ECE, Portland State University, Portland, -AOR3, United States
语种	英语
WOS记录号	WOS:000329132400008
引用统计
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16889
专题	中国科学院软件研究所
通讯作者	Li, Y.(lyj238@gmail.com)
推荐引用方式 GB/T 7714	Li, Yongjian ,Zeng, Naiju ,Hung, William N.N. ,et al. Combining symmetry reduction with generalized symbolic trajectory evaluation[J]. Computer Journal,2014,57(1):115-128.
APA	Li, Yongjian ,Zeng, Naiju ,Hung, William N.N. ,Song, Xiaoyu ,&Li, Y..(2014).Combining symmetry reduction with generalized symbolic trajectory evaluation.Computer Journal,57(1),115-128.
MLA	Li, Yongjian ,et al."Combining symmetry reduction with generalized symbolic trajectory evaluation".Computer Journal 57.1(2014):115-128.