Hardware verification algorithms were previously modified to suit software verification and implemented in CPAchecker. These algorithms iteratively compute interpolants to overapproximate reachable state space and eventually converge to invariant. They use interpolation in a so-called forward fashion to overapproximate reachable states from initial states. Dual Approximated Reachability algorithm also uses interpolants to overapproximate states that can reach assertion-violating states. It combines information from both forward and backward interpolation sequences to converge faster. In the talk, we briefly explain the main idea of the algorithm, show practical obstacles in the CPAchecker implementation that we overcame and present the final results of the algorithm’s performance.

Marek Jankola

LMU Munich