language-theoretic abstraction refinement

ISCAS OpenIR

	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
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	362-376
会议日期	March 24, 2012 - April 1, 2012
会议地点	Tallinn, Estonia
收录类别	EI
ISSN	0302-9743
ISBN	9783642288715
部门归属	(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
摘要	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.
关键词	Algorithms Verification
主办者	Institute of Cybernetics at TUT; "Tallinn University of Technology(TUT)"; EXCS Eur. Reg. Dev. Fund (ERDF); Estonian Convention Bureau; Microsoft Research
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15687
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Long Zhenyue,Calin Georgel,Majumdar Rupak,et al. language-theoretic abstraction refinement[C],2012:362-376.