Strategy Selection for Software Verification Based on Boolean Features A Simple but Effective Approach

扫码查看

原文链接

NETL

外文摘要：Software verification is the concept of determining， given an input program and a specification， whether the input program satisfies the specification or not。 There are different strategies that can be used to approach the problem of software verification， but， according to comparative evaluations， none of the known strategies is superior over the others。 Therefore， many tools for software verification leave the choice of which strategy to use up to the user， which is problematic because the user might not be an expert on strategy selection。 In the past， several learning-based approaches were proposed in order to perform the strategy selection automatically。 This automatic choice can be formalized by a strategy selector， which is a function that takes as input a model of the given program， and assigns a verification strategy。 The goal of this paper is to identify a small set of program features that (1) can be statically determined for each input program in an efficient way and (2) sufficiently distinguishes the input programs such that a strategy selector for picking a particular verification strategy can be defined that outperforms every constant strategy selector。 Our results can be used as a baseline for future comparisons， because our strategy selector is simple and easy to understand， while still powerful enough to outperform the individual strategies。 We evaluate our feature set and strategy selector on a large set of 5 687 verification tasks and provide a replication package for comparative evaluation。

外文关键词：

Strategy selectionSoftware verificationAlgorithm selectionProgram analysisModel checking

作者：

Dirk Beyer、Matthias Dangl

展开 >

作者单位：

LMU Munich, Germany

会议名称：

International symposium on leveraging applications of formal method, verification and validation

会议地点：

Limassol(CY)

会议母体文献：

Leveraging applications of formal methods, verification and validation: verification

页码：

144-159

出版时间：

2018

DOI：

10.1007/978-3-030-03421-4_11