Interpolant-Based Transition Relation Approximation

TL;DR

This paper introduces an interpolant-based technique to strengthen transition relation approximations in predicate abstraction, ensuring convergence without exact image computation and demonstrating faster convergence empirically.

Contribution

It presents a novel interpolant-based method for improving transition relation approximation in predicate abstraction, guaranteeing convergence with fewer calls to decision procedures.

Findings

Method converges faster than previous counterexample-based approaches.

Guarantees convergence given an adequate predicate set.

Reduces exponential complexity in image computation.

Abstract

In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given an adequate set of predicates. We present an interpolant-based method for strengthening the abstract transition relation in case of such failures. This approach guarantees convergence given an adequate set of predicates, without requiring an exact image computation. We show empirically that the method converges more rapidly than an earlier method based on counterexample analysis.