Language-Theoretic Abstraction Refinement
Language-Theoretic Abstraction Refinement
复制标题
语言理论抽象细化
DOI：
10.1007/978-3-642-28872-2_25
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
R. Meyer
中科院分区：
文献类型：
--
作者：
Zhenyue Long;Georgel Calin;R. Majumdar;R. Meyer
我们提供了一种语言理论反例引导的抽象精致（CEGAR）算法，以对递归多线程程序进行安全验证。首先，我们将安全验证减少到无上下文语言交集的（不可决定的）语言空虚问题。最初，我们的CEGAR程序过度贴上了通过无上下文的语言的交叉点。如果过度应用是空的，我们将声明系统安全。否则，我们从过度应用中计算一个有界的语言，并检查空虚的自由语言和有限语言的交集（这是可决定的）。如果交集是非空的，我们将报告一个错误。如果空的，我们通过删除有界语言并重试来完善过度应用。 CEGAR循环的关键思想是语言理论观点：定期过度应用和交叉点限制的不同策略提供了不同的实现。我们为使用普通语言近似于无上下文的语言提供具体算法，并生成代表反描述家庭的有限语言。我们已经实施了算法，并就常规过度Ximimation和有限的不足耐毒性进行了各种选择提供了实验比较。
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.