As it turns out, this doesn't actually work. State derived program analysis has been shown to not be provable for all cases. Particularly when the state-space i

As it turns out, this doesn't actually work. State derived program analysis has been shown to not be provable for all cases. Particularly when the state-space is very large, and when state transitions are non-atomic in the code, e.g. two or more state transitions in a code block. The best research I've seen on this was done with Access Control Matrices in the Computer Security field. e.g. can you prove in a general sense that a sequence of atomic state changes to an ACM result in no violations of access control? The answer is, for atomic state changes you can prove that they are internally consistent, but not that they do not introduce a flaw in the ACM. In other words, because proving software reduces to proving correctness, it only proves that the software is internally consistent. Basically it's a circular proof. It doesn't prove that the software is without flaw.