Software verification

Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements.

Broad scope and classification

A broad definition of verification makes it related to software testing. In that case, there are two fundamental approaches to verification:

Dynamic verification, also known as experimentation, dynamic testing or, simply testing. - This is good for finding faults (software bugs).
Static verification, also known as analysis or, static testing - This is useful for proving the correctness of a program. Although it may result in false positives when there are one or more conflicts between the process a software really does and what the static verification assumes it does.

Under the ACM Computing Classification System, software verification topics appear under "Software and its engineering", within "Software creation", whereas Program verification also appears under Theory of computation under Semantics and reasoning, Program reasoning.

IEEE: SWEBOK: Guide to the Software Engineering Body of Knowledge
Carlo Ghezzi, Mehdi Jazayeri, Dino Mandrioli: Fundamentals of Software Engineering, Prentice Hall, ISBN 0-13-099183-X
Alan L. Breitler: A Verification Procedure for Software Derived from Artificial Neural Networks, Journal of the International Test and Evaluation Association, Jan 2004, Vol 25, No 4.
Vijay D'Silva, Daniel Kroening, Georg Weissenbacher: A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7): 1165-1178 (2008)