> interesting fundamental CS research (especially into automated verification/program correctness/security) these days As far as I know they are doing it for l

> interesting fundamental CS research (especially into automated verification/program correctness/security) these days As far as I know they are doing it for looong time (look at Spec# for example). They needed it for the driver WHQL verification (they actually verify that the drivers fulfill some temporal logic predicates)