Interesting, have you also looked at other formal methods, like Abstract Interpretation?