Institutional Repository
| 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 | |
| Source | Computer Journal
 |
| ISSN | 104620 |
| Volume | 57Issue:1Pages:115-128 |
| English Abstract | 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. |
| Indexed Type | SCI ; EI |
| Keyword | Generalized Symbolic Trajectory Evaluation Symmetry Reduction Theorem Proving |
| Department | (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 |
| Language | 英语 |
| WOS ID | WOS:000329132400008 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16889 |
| Collection | 中国科学院软件研究所 |
| Corresponding Author | Li, Y.(lyj238@gmail.com) |
| Recommended Citation 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. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment