language-theoretic abstraction refinement
文献类型：会议论文
| 作者 | Long Zhenyue ; Calin Georgel ; Majumdar Rupak ; Meyer Roland |
| 出版日期 | 2012 |
| 会议名称 | 15th International Conference on Fundamental Approaches to Software Engineering, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012 |
| 会议日期 | March 24, 2012 - April 1, 2012 |
| 会议地点 | Tallinn, Estonia |
| 关键词 | Algorithms Verification |
| 页码 | 362-376 |
| 中文摘要 | We give a language-theoretic counterexample-guided abstraction refinement (CEGAR) algorithm for the safety verification of recursive multi-threaded programs. First, we reduce safety verification to the (undecidable) language emptiness problem for the intersection of context-free languages. Initially, our CEGAR procedure overapproximates the intersection by a context-free language. If the overapproximation is empty, we declare the system safe. Otherwise, we compute a bounded language from the overapproximation and check emptiness for the intersection of the context free languages and the bounded language (which is decidable). If the intersection is non-empty, we report a bug. If empty, we refine the overapproximation by removing the bounded language and try again. The key idea of the CEGAR loop is the language-theoretic view: different strategies to get regular overapproximations and bounded approximations of the intersection give different implementations. We give concrete algorithms to approximate context-free languages using regular languages and to generate bounded languages representing a family of counterexamples. We have implemented our algorithms and provide an experimental comparison on various choices for the regular overapproximation and the bounded underapproximation. © 2012 Springer-Verlag Berlin Heidelberg. |
| 英文摘要 | We give a language-theoretic counterexample-guided abstraction refinement (CEGAR) algorithm for the safety verification of recursive multi-threaded programs. First, we reduce safety verification to the (undecidable) language emptiness problem for the intersection of context-free languages. Initially, our CEGAR procedure overapproximates the intersection by a context-free language. If the overapproximation is empty, we declare the system safe. Otherwise, we compute a bounded language from the overapproximation and check emptiness for the intersection of the context free languages and the bounded language (which is decidable). If the intersection is non-empty, we report a bug. If empty, we refine the overapproximation by removing the bounded language and try again. The key idea of the CEGAR loop is the language-theoretic view: different strategies to get regular overapproximations and bounded approximations of the intersection give different implementations. We give concrete algorithms to approximate context-free languages using regular languages and to generate bounded languages representing a family of counterexamples. We have implemented our algorithms and provide an experimental comparison on various choices for the regular overapproximation and the bounded underapproximation. © 2012 Springer-Verlag Berlin Heidelberg. |
| 收录类别 | EI |
| 会议主办者 | Institute of Cybernetics at TUT; "Tallinn University of Technology(TUT)"; EXCS Eur. Reg. Dev. Fund (ERDF); Estonian Convention Bureau; Microsoft Research |
| 会议录 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
 |
| 语种 | 英语 |
| ISSN号 | 0302-9743 |
| ISBN号 | 9783642288715 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/15687]  |
| 专题 | 软件研究所_软件所图书馆_会议论文 |
| 推荐引用方式 GB/T 7714 | Long Zhenyue,Calin Georgel,Majumdar Rupak,et al. language-theoretic abstraction refinement[C]. 见:15th International Conference on Fundamental Approaches to Software Engineering, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. Tallinn, Estonia. March 24, 2012 - April 1, 2012. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。