“In all affairs it’s a healthy thing now and then to hang a question mark on the things you have long taken for granted.”
|--(Bertrand Russell, 1872–1970)|
Arguably, the most powerful tool we have in our arsenal for the verification of software applications is logical abstraction. By capturing the essence of a design in a mathematical model, we can often demonstrate conclusively that the design has certain inevitable properties. The purpose of a verification model, then, is to enable proof. If it fails to do so, within the resource limits that are available to the verification system, the model should be considered inadequate.
The type of abstraction that is appropriate for a given application ...