[gumby]

That's a good question -- I should not have been so terse/flip. I agree they do find some interesting issues and that's why I liked the paper.

On the practicality side: If I read the paper correctly this is a lint like tool for finding suspected problems (hence e.g. the "litmus tests" -- the tool iterates out the possible states, which is great). It isn't a tool for finding new problems. The compiler testing is interesting (I'm an former compiler guy) but reading Sec 7 didn't lead me to believe it could identify code generation problems in cases of very high optimizations.

Also a lot of recent security issues have been in the implementation of the microarchitecture (not just microcode bugs but functional unit errors such as the recent hyper threading leaks).

Maybe I am being too harsh?