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.