Kenneth McMillan and Andrey Rybalchenko
17 January 2013
We present a interpolation-based method for symbolically comput- ing 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 im- plemented in tool called Duality, which we evaluate using device driver verification benchmarks.