Avoiding exponential explosion: generating compact verification conditions
Avoiding exponential explosion: generating compact verification conditions
复制标题
DOI：
10.1145/360204.360220
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
C. Flanagan;J. Saxe
中科院分区：
文献类型：
--
作者：
C. Flanagan;J. Saxe
当前的验证条件（VC）生成算法，例如最弱的先决条件，产生了一个VC，其大小可能在被检查的代码片段的大小上指数呈指数。本文描述了一种两阶段的VC生成算法，该算法生成了紧凑的VC，其大小在源片段的尺寸上是最差的二次二次，并且在实践中接近线性。这两个阶段的VC生成算法已被作为作为一部分Java的扩展静态检查器。它使我们能够检查大型且复杂的方法，否则由于时间和空间限制，无法检查。
Current verification condition (VC) generation algorithms, such as weakest preconditions, yield a VC whose size may be exponential in the size of the code fragment being checked. This paper describes a two-stage VC generation algorithm that generates compact VCs whose size is worst-case quadratic in the size of the source fragment, and is close to linear in practice.This two-stage VC generation algorithm has been implemented as part of the Extended Static Checker for Java. It has allowed us to check large and complex methods that would otherwise be impossible to check due to time and space constraints.