Indeed it is. What I'm working toward is a more efficient way to do the same, that doesn't take the touted 30 man years of effort to accomplish. I'm working on

Indeed it is. What I'm working toward is a more efficient way to do the same, that doesn't take the touted 30 man years of effort to accomplish. I'm working on a hybrid approach between SMT solving and constructive proofs. Model checking done with an SMT solver is pretty sound. I'm actually planning a book on a scalable technique to do this with CBMC. But, the last leg of this really is understanding the compiler output.