Institutional Repository
| environment abstraction with state clustering and parameter truncating | |
| Pan Hong; Lv Yi; Lin Huimin | |
| 2009 | |
| Conference Name | 3rd International Symposium on Theoretical Aspects of Software Engineering |
| Source | Proceedings - 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 |
| Conference Date | JUL 29-31, |
| Conference Place | Tianjin, PEOPLES R CHINA |
| Publish Place | 10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA |
| Publisher | THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS |
| ISBN | 978-0-7695-3757-3 |
| Department | Pan, Hong; Lv, Yi; Lin, Huimin Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing 100190, Peoples R China. |
| English Abstract | 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. |
| Keyword | Computer Software Model Checking |
| Sponsorship | IEEE Comp Soc, IFIP, Tianjin Normal Univ |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/8304 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation 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. |
| 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