1 Verification Approach

Composing verification techniques in sequence has in the past been a promising approach in the annual software verification competition SV-COMP. Especially in 2018Footnote 1, the software verification framework CPAchecker [3], using a composition of analyses, was able to outperform competitors in category ReachSafety. However, the analysis sequence is often predefined and fixed. In other words, a problem instance might pass through a sequence of unsuccessful verification configurations until it is processed by the right technique or exceeds a time limit.

Our competition contribution utilizes the sequential setting of CPAchecker (more precisely, of CPA-Seq), but predicts the order of verification tools viz. configurations. For this, we applied an extension of our rank prediction approach introduced in [7]. Basically, for a given verification task we predict an ordering of CPAchecker configurations, and then sequentially run these configurations. Configurations are ordered with respect to their (likely) performance on the verification task.

The prediction employs machine learning. For the learning, we extract features of verification tasks via an encoding of programs as graphs combining concepts of control-flow and program dependence graphs with abstract syntax trees. Features represent certain graph substructures of programs, where the depth of substructures considered is configurable.

To obtain the execution order for a new problem instance, the Ranking by pairwise comparison (RPC) [9] framework is employed utilizing kernelized Support Vector Machines (SVM) [11] as base learners. By employing SVMs, we are able to choose a kernel functionFootnote 2 (similar to Weisfeiler-Lehman kernels [12]) that is specifically designed for graph substructures. However, the function proposed in [7] needed to be computed between the input instance X (the graph of a verification task) and every training sample Y, which can be quite costly in practice. As a consequence, we have re-implemented this approach and now compute Weisfeiler-Lehman-based features of single graphs. This significantly improves the performance of prediction.

2 Software Architecture

Our tool contribution PeSCo embeds a Planning step in the restart algorithm employed in the verification framework CPAchecker [3]. The restart algorithm [10] is used in a sequential combination of verifiers to let the next verifier start on already computed (partial) results of previous verifiers, in particular when the previous verifier could not solve the verification problem. However, instead of executing a fixed list of verification techniques, our algorithm plans an execution order dependent on the verification task to be solved. Our approach consists of the following steps.

  • Training. To train our rank predictor, we employ rankings obtained by executing 5 CPAchecker configurations on the verification tasks of SV-COMP 2018. Similar to CPA-Seq [10] from 2018, we use Value Analysis [5], Value Analysis + CEGAR [5], Predicate Analysis [4], k-Induction [1] and Bounded Model Checking [6]. In addition, we introduced and carried out training with a special UNKNOWN configuration. This extension will allow our prediction procedure to cut off an analysis when it will most probably fail.

  • Planning. As can be seen in Fig. 1, we utilize the preprocessor and control flow automaton (CFA) construction implemented in CPAchecker. Instead of passing the CFA directly to an analysis, we first query our rank prediction process. The prediction process starts by building an intermediate graph representation. This is followed by a feature extraction and the final ranking procedure (details in [7]). If a prediction is not achievable in a certain time frame, we fall back to the standard CPA-Seq.

  • Execution. After planning a sequential composition, we can apply the analyses in the given order. If an analysis fails or exceeds its time limit, we switch to the next configuration. On reaching the UNKNOWN configuration, we exit the verification sequence. Instead of leaving the overall process, specialized techniques will be applied in the following situations: For recursive programs we facilitate Block Abstraction Memoization (BAM) [8, 13] and Binary Decision Diagrams (BDD) [2] are used for concurrent programs. Witnesses are written as generated by the verifiers.

Despite the fact that our implementation is only dependent on Java 8, we need MathSAT 5Footnote 3 to run individual configurations. Furthermore, parser frontend for C programs are used according to CPAchecker.

Fig. 1.
figure 1

Architecture of PeSCo implemented within CPAchecker. The dotted box represent the Restart Algorithm enhanced by our rank prediction. Hence, Analysis II receives partial results of Analysis I for a restart of the verification. The rank prediction utilizes the control flow automaton extended by data and control dependencies (PDG).

Full size image

3 Strengths and Weaknesses

In contrast to traditional compositional approaches, PeSCo adapts to the given tasks. As a result, our tool is able to decrease the runtime by skipping techniques that do not fit to the given verification task. More importantly, the adaptation allows us to omit analyses which introduce failures. Consequently, PeSCo improves the number of correct results in a given time frame.

Nevertheless, learning the optimal ranking requires time and introduces uncertainty to the verification process. Experiments on 1148 tasks in ReachSafety-ECA show that optimal rankings on a large number of similar programs with different requirements are difficult to predict. Still, the results of SV-COMP 2019 show that PeSCo can effectively verify a number of C programs in that category.

Due to the prediction process, PeSCo is furthermore limited to the configurations that occur during training. Since we trained our predictor with the version of CPAchecker employed in SV-COMP 2018, we perform slightly worse than the improved 2019 version of CPA-Seq.

4 Tool Setup and Configuration

PeSCo is fully integrated in the official source code of CPAchecker. Thus, it can be downloaded as a fork: https://github.com/cedricrupb/cpachecker. We use Revision b8d6131 for the competition. To compile the tool, ant should be executed on the checkout folder. After this step, our tool requires Java 8 and MathSAT 5 as external tools. To verify a test program, CPAchecker is executed with the following command line:

figure a

For programs expecting a 64 Bit model, add the parameter . PeSCo participates in category ReachSafety, Falsification and Overall. The corresponding specification can be found in the checkout folder under

config/specification/sv-comp-reachability.spc.

5 Software Project and Contributors

Being an extension of the CPAchecker project, PeSCo is developed as an open-source project by a research group from Paderborn University. Contributors were so far Mike Czech, Marie-Christine Jakobs, Cedric Richter and Heike Wehrheim. We would furthermore like to thank Eyke Hüllermeier for machine learning expertise and his contribution to the prediction process. We aso thank the CPAchecker team for allowing us to use their tool.