Verification by Gambling on Program Slices

Automated software verification is a computationally hard problem that is often exasperated by irrelevant context. Existing verification engines address this problem with slicing techniques that are either too cautious, producing large verification condition queries, or too aggressive, sacrificing soundness. In this paper, we present a novel technique, called Qicc, that is aggressive, sound, and “a little risky.” Specifically, we use procedure extraction to generate a small set of verification queries that we check with existing verification engines. If any query in the set passes verification, then the original program will pass verification. However, there is no guarantee that such a query will exist, so Qicc may waste time searching. We study the effectiveness of Qicc when it is combined with two different verification engines, finding that Qicc’s extra cost is small while the rewards it brings to the analysis are significant. We evaluated Qicc on a case study—the verification of a cryptographic function in BusyBox—and found that Qicc succeeds when paired with two different verifiers, while both verifiers are unsuccessful on their own.