[0815test]

> (Bounded) model checking

Oh come on. If your bounded model checking is actually checking every possible input or program state, then it's not just a method of verification but an actual proof. (It may be a subjectively inelegant proof, but it's a proof nonetheless.) That much is obvious. What I clearly meant by "glorified fuzzing" was the far more common use of model checking in ways that stop short of this standard. That sort of use can still be nicely scalable, it does count as a formal method, and it can point out remarkably complex bugs in your system - but by definition, it cannot give any assurance that you're doing things correctly! That still requires proof.

[tempguy9999]

To put my oar in, and this is purely based on what I've read about spin, spin can verify 100% for 'small' models. If larger models are checked, it will run out of memory so you put it in a probabilistic mode which gives probabilistic assurances, still 'good' but less than 100%. In that respect I suppose it's degenerated to rather posh fuzzing.

I think the difference between small and large is down to how long you're prepared to let it run, but even more fundamentally, how much memory you can give it.

I'd agree that if the model matches the code and you successfully check the entire state space then it's a proof.