Institutional Repository
| language-theoretic abstraction refinement | |
| Long Zhenyue; Calin Georgel; Majumdar Rupak; Meyer Roland | |
| 2012 | |
| Conference Name | 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 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 362-376 |
| Conference Date | March 24, 2012 - April 1, 2012 |
| Conference Place | Tallinn, Estonia |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642288715 |
| Department | (1) Max Planck Institute for Software Systems Germany; (2) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China; (3) Graduate University Chinese Academy of Sciences China; (4) Department of Computer Science University of Kaiserslautern Germany |
| English Abstract | 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. |
| Keyword | Algorithms Verification |
| Sponsorship | Institute of Cybernetics at TUT; "Tallinn University of Technology(TUT)"; EXCS Eur. Reg. Dev. Fund (ERDF); Estonian Convention Bureau; Microsoft Research |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15687 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Long Zhenyue,Calin Georgel,Majumdar Rupak,et al. language-theoretic abstraction refinement[C],2012:362-376. |
| 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