* [[Formal verification#Formal verification for software|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.
=== Formal Verification ===
Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Subareas of formal verification include [[abstract interpretation]], [[automated theorem proving]], [[type system]]s, and [[formal methods#Lightweight formal methods|lightweight formal methods]].
These techniques can be ''[[soundness|sound]]'', meaning that the verified properties can be logically deduced from the semantics, or ''unsound'', meaning that there is no such guarantee. A sound technique yields a result only once it has searched the entire space of possibilities. An example of an unsound technique is one that searches only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result. We also talk about whether these techniques are ''[[decidability|decidable]]'', whether they are guaranteed to terminate with an answer. Because they are bounded, unsound techniques are often more likely to be decidable than sound ones.
