Sliced Path Prefixes: An Effective Method to Enable Refinement Selection
Sliced Path Prefixes: An Effective Method to Enable Refinement Selection
复制标题
切片路径前缀：启用细化选择的有效方法
DOI：
10.1007/978-3-319-19195-9_15
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Philipp Wendler
中科院分区：
文献类型：
--
作者：
Dirk Beyer;Stefan Löwe;Philipp Wendler
自动软件验证依赖于为给定的程序构建一个抽象模型，该模型（1）足够抽象以避免状态空间爆炸，（2）足够精确以推理规范。反例引导的抽象细化是一种标准技术，它建议从不可行的错误路径中提取信息，以便在抽象模型太不精确时对其进行细化。现有的方法-包括我们以前的工作-不选择一个给定的路径系统的细化。我们提出了一种方法，产生替代细化，并允许系统地选择一个合适的。该方法以一个给定的不可行的错误路径作为输入，并应用切片技术来获得一组新的错误路径，这些错误路径比原始错误路径更抽象，但仍然是不可行的，每个错误路径都有不同的原因。新路径的（更抽象的）约束可以传递到一个标准的细化过程，以获得一组可能的细化，每个新path. Our技术是完全独立的抽象域中使用的程序分析，并不依赖于一定的证明技术，如SMT解决。我们在验证框架CPAchecker中实现了新算法，并公开了我们的扩展。我们的技术的实验评估表明，有一个广泛的可能性，如何细化的抽象模型为一个给定的错误路径，我们证明了选择的细化应用到抽象模型的验证有效性和效率有显着的影响。
Automatic software verification relies on constructing, for a given program, an abstract model that is (1) abstract enough to avoid state-space explosion and (2) precise enough to reason about the specification. Counterexample-guided abstraction refinement is a standard technique that suggests to extract information from infeasible error paths, in order to refine the abstract model if it is too imprecise. Existing approaches —including our previous work— do not choose the refinement for a given path systematically. We present a method that generates alternative refinements and allows to systematically choose a suited one. The method takes as input one given infeasible error path and applies a slicing technique to obtain a set of new error paths that are more abstract than the original error path but still infeasible, each for a different reason. The (more abstract) constraints of the new paths can be passed to a standard refinement procedure, in order to obtain a set of possible refinements, one for each new path. Our technique is completely independent from the abstract domain that is used in the program analysis, and does not rely on a certain proof technique, such as SMT solving. We implemented the new algorithm in the verification frameworkCPAcheckerand made our extension publicly available. The experimental evaluation of our technique indicates that there is a wide range of possibilities on how to refine the abstract model for a given error path, and we demonstrate that the choice of which refinement to apply to the abstract model has a significant impact on the verification effectiveness and efficiency.