Computing Relational Fixed Points using Interpolation

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.

MSR-TR-2013-6.pdf
PDF file

Details

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