Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that — despite the necessity of exchanging complex data via interfaces — the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.
We provide the following content:
Our implementation of C-CEGAR in CoVeriTeam is available on GitLab.
Decomposing an existing CEGAR implementation into components has (almost) no negative effects on the effectiveness of the approach. Moreover, the new tool can have a higher precision because better components can be used.
The efficiency of C-Pred decreases only by a constant factor (median smaller than three).
The above plot (Figure 10a in the paper) shows the run time
required by traditional, tightly coupled predicate abstraction in
CPAchecker (Pred, x-axis), and the decomposed version in C-CEGAR
(C-Pred, y-axis). Run time is measured in CPU time seconds.
The above plot (Figure 10b in the paper) shows the
distribution of the run-time factor (the increase in runtime) for
C-Pred, compared to Pred.
The above plot (extended version of Figure 11 in the paper)
shows the median factor of run-time increase by C-Pred compared to Pred,
grouped by the number of required CEGAR iterations. The width of the bar
for i corresponds to the number of verification tasks that
require exactly i CEGAR iterations.
The effectiveness of C-CEGAR reduces by 20% when using standardized formats, whereas the efficiency is not influenced.
The above plot (Figure 13 in the paper) compares the run
time required by two versions of the decomposed predicate abstraction in
C-CEGAR: C-Pred (x-axis) uses the proprietary predicate map for
precision exchange, and C-PredWit (y-axis) uses the standardized format
for correctness witnesses. Run time is measured in CPU time seconds.
C-CEGAR allows a simple exchange of feasibility checkers. The use of conceptually different off-the-shelf checkers can increase the effectiveness of C-CEGAR
C-CEGAR allows a simple exchange of precision refiners. The use of conceptually different off-the-shelf refiners can increase the effectiveness of C-CEGAR.
More details are available in our research paper.
