Reusing Precisions for Efficient Regression Verification
This addresses the impracticality of continuous verification for software developers, though it is incremental as it builds on existing precision-based methods.
The paper tackles the problem of high resource consumption in continuous model checking by reusing abstraction precisions, showing experimentally that this approach reduces verification effort on 59 Linux device drivers with 1119 revisions.
Continuous testing during development is a well-established technique for software-quality assurance. Continuous model checking from revision to revision is not yet established as a standard practice, because the enormous resource consumption makes its application impractical. Model checkers compute a large number of verification facts that are necessary for verifying if a given specification holds. We have identified a category of such intermediate results that are easy to store and efficient to reuse: abstraction precisions. The precision of an abstract domain specifies the level of abstraction that the analysis works on. Precisions are thus a precious result of the verification effort and it is a waste of resources to throw them away after each verification run. In particular, precisions are small and thus easy to store; they are easy to process and have a large impact on resource consumption. We experimentally show the impact of precision reuse on industrial verification problems, namely, 59 device drivers with 1119 revisions from the Linux kernel.