  Software systems evolve throughout their life cycles. Many revisions are
produced over time. Model checking each revision of the software is
impractical. Regression verification suggests reusing intermediate results from
the previous verification runs. This paper proposes a fully automatic
regression verification technique in the context of CEGAR. Procedure summaries,
which describe the input/output behaviors of a procedure, are proposed as the
intermediate results to be reused. Procedure summaries are reasonably small to
store, technically easy to process, and do not require much extra computation
effort to be reused. Reusing procedure summaries saves much analysis effort on
the corresponding procedures. By combining regression verification and CEGAR,
we propose a technique that is able to reuse procedure summaries across
different abstract precisions and different program revisions. We performed
extensive experiments on a large number of industrial programs (534 revisions
of 89 Linux kernel device drivers). The results show that our approach can
significantly improve the performance of regression verification.
