OK, so I went back and re-read that paragraph twice more. I'm not sure if the claim is about abstract interpretation, model checking, or the particular problem domain, but I'm quite certain that Microsoft's tool can't claim novelty in implementing any of those, or even all three together.