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.

VMCAI09: Mostly-Functional Behavior in Java Programs

it propose a type and effect system that can find out "run time constance" variables in JAVA.

I remember that I read a related paper a couple of  months before, that paper discuss "stationary" field, which is similar to to this.

similar mechnism include the java standard "final" field, which is some what too restricted.

So in summary, there are three class of such mechnism:

final,too strong

stationary

quie scing

Such mechnism can prevent those variables from been initialied or writen more than one time.typical application include OO system that need to initite newlly allocated object.

Its slide describe an interesting relation between type system and effect system, the formmer one describe "what is the object",while the later one describe "how the object behave"