Software Verification Tools

This text explores the problem of verifying software in terms of a set of simple tools which can be used to symbolically evaluate and prove properties of pieces of programs, represented either abstractly in functional terms, or by actual text. The tools can be thought of as roughly analogous to spelling and style checkers in word-processing; they reduce the labor of finding errors and provide some semi-automated aids to making corrections.