VMCAI'10:Interpolant Strength

This paper propose two approaches to generate a family of interpolants with different strength.

One approach based on labeling function, which will how to mark the internal node of a proof tree, and different function corresponding to different existing interpolant system.

And the other approach "swap" demonstrate that, by changing the order of clause the take part in the resolution, different interpolant can be obtained.

But this paper do not say how to select which strength to be used to boost model checking performance.

Come back again

after 9 months of blockage by GFW, I manage to go through it with Tor.

I will now begin to update my blog again.