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.

PDF file

Details