A Framework for State and Trace Interpolation

Duc-Hiep Chu and Joxan Jaffar

Abstract

We address the problem of reasoning about interleavings in safety verification of concurrent programs. In the literature, there are two prominent techniques for pruning the search space. First, there is \emph{state-based} interpolation where a collection of formulas can be generalized by taking into account the property to be verified. Second, there are \emph{trace-based} methods, collectively known as ``Partial Order Reduction (\por{})'', which operate by weakening the concept of a trace by abstracting the total order of its transitions into a partial order. Our main contribution is a framework that \emph{synergistically} combines state interpolation with \por{} so that the sum is more than its parts.