Comment Re:Just moves the errors up one level (Score 5, Informative) 66
The purpose of model checking is rarely to specify the whole behavior of the program, but to ensure that some condition are always true or false. Such condition can be the absence of buffer overflow ... relatively easy to formulate, hard to discover ...
