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.
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.

Dynamic verification (Test, experimentation)

Dynamic verification is performed during the execution of software, and dynamically checks its behavior; it is commonly known as the Test phase.
Verification is a Review Process.
Depending on the scope of tests, we can categorize them in three families:

Test in the small: a test that checks a single function or class
Test in the large: a test that checks a group of classes, such as
* Module test
* Integration test
* System test
Acceptance test: a formal test defined to check acceptance criteria for a software
* Functional test
* Non functional test

The aim of software dynamic verification is to find the errors introduced by an activity ; or by the repetitive performance of one or more activities.

Static verification (Analysis)

Static verification is the process of checking that software meets requirements by inspecting the code before it runs. For example:

Code conventions verification
Bad practices detection
Software metrics calculation
Formal verification

Verification by Analysis - The analysis verification method applies to verification by investigation, mathematical calculations, logical evaluation, and calculations using classical textbook methods or accepted general use computer methods. Analysis includes sampling and correlating measured data and observed test results with calculated expected values to establish conformance with requirements.

Narrow scope

When it is defined more strictly, verification is equivalent only to static testing and it is intended to be applied to artifacts. And, validation would be equivalent to dynamic testing and intended to be applied to the running software product. Notice that requirements validation can be performed statically and dynamically.

Comparison with validation

Software verification is often confused with software validation. The difference between verification and validation:

Software verification asks the question, "Are we building the product right?"; that is, does the software conform to its specifications?
Software validation asks the question, "Are we building the right product?"; that is, does the software do what the user really requires?