Thread-Modular Verification Is Cartesian Abstract Interpretation
Thread-Modular Verification Is Cartesian Abstract Interpretation
复制标题
线程模块化验证是笛卡尔抽象解释
DOI：
10.1007/11921240_13
复制
发表时间：
2006
影响因子：
0.8
通讯作者：
A. Rybalchenko
中科院分区：
文献类型：
--
作者：
A. Malkis;A. Podelski;A. Rybalchenko
多线程程序的验证是困难的。它需要对并发线程数量呈指数级增长的状态空间进行推理。基于线程行为过度近似的模块化组合的成功验证技术已经被设计用于此任务。这些技术传统上以假设-保证方式描述，这种方式不允许对所涉及的组合论证的抽象属性进行推理。Flanagan and Qadeer线程模块化算法是这类技术的典型代表。本文在抽象解释的框架下研究了该算法的形式化。我们确定算法实现的元素；它的定义涉及集合的笛卡尔积。研究结果为系统研究处理状态爆炸问题的类似抽象提供了基础。作为这个方向的第一步，我们的结果提供了Flanagan和Qadeer算法精度的最小增加的特征，导致其多项式复杂性的损失。
Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of over-approximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the ion that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, our result provides a characterization of a minimal increase in the precision of the Flanagan and Qadeer algorithm that leads to the loss of its polynomial complexity.