Computing Relational Fixed Points using Interpolation

We present a interpolation-based method for symbolically computing relational post-fixed points. The method can be used to solve for unknown predicates in the verification conditions of programs. Thus, it has a variety of applications, including including model checking of recursive and threaded programs. The method is implemented in tool called Duality, which we evaluate using device driver verification benchmarks.