Computing Relational Fixed Points using Interpolation

Kenneth McMillan and Andrey Rybalchenko

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2013-6
> Publications > Computing Relational Fixed Points using Interpolation