A pleasant surprise seeing an Alastair Donaldson supported paper. What I liked most at Imperial was the amount of professors pushing for things that sat between the fully theoretical world, and the more real engineering world. From a first quick skim this paper seems to hit that right on the head. I've been wanting to see how I could introduce more of the fun of formal verification into my job, so I'll be digging deep into this one for some inspiration.