Lazy abstraction
Lazy abstraction
复制标题
DOI：
10.1145/503272.503279
复制
发表时间：
2002-01
期刊：
影响因子：
--
通讯作者：
T. Henzinger;Ranjit Jhala;R. Majumdar;G. Sutre
中科院分区：
文献类型：
--
作者：
T. Henzinger;Ranjit Jhala;R. Majumdar;G. Sutre
一种软件模型检测方法基于抽象 - 检测 - 精化范式：构建一个抽象模型，然后检测所需属性，如果检测失败，则精化模型并重新开始。我们引入惰性抽象的概念来整合和优化抽象 - 检测 - 精化循环的三个阶段。惰性抽象由模型检测程序驱动，根据需求持续构建和精化单个抽象模型，使得模型的不同部分可以呈现不同的精度程度，即刚好足以验证所需属性。我们提出一种使用惰性抽象检测安全属性的算法，并描述该算法应用于C程序的一个实现。我们还提供了该方法终止的充分条件。
One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.