Other meanings of Program verification
Computer science
Program verification is the formal verification that software programs satisfy specified properties. It uses mathematical models, logical reasoning, and mechanically checked proofs to establish claims about behavior, such as functional correctness, safety, termination, or adherence to a protocol. Unlike testing, which examines selected executions, verification reasons about all executions covered by the model and assumptions. Its central challenge is expressing requirements precisely enough to prove while keeping the program, specification, and proof tractable.
Program verification establishes that a program satisfies a formally stated specification under stated assumptions. A specification may describe input-output behavior, invariants that must always hold, permitted security flows, resource bounds, or termination. The result is conditional: a proof is only as strong as its model, requirements, compiler assumptions, and trusted components.
Hoare logic, introduced by C. A. R. Hoare, expresses correctness with triples of the form {precondition} program {postcondition}. Variants and loop invariants allow a verifier to reason compositionally about procedures and iteration.1 Verification therefore differs from validation and testing: tests provide evidence from chosen cases, whereas a successful proof can cover every execution represented by the formal model.
Typical properties include memory safety, absence of arithmetic errors, functional equivalence, access-control rules, and protocol conformance. Verification can target source code, intermediate representations, compiled code, or hardware-software combinations.
The principal methods trade expressive power, automation, and proof effort in different ways. Deductive verification generates logical obligations from program statements, assertions, and invariants; interactive theorem provers or automated solvers then discharge those obligations. Systems such as Dafny, Why3, and verification extensions for proof assistants support this style, often requiring programmers to supply specifications and intermediate lemmas.
Model checking explores the state space of a finite or finitely abstracted transition system and checks temporal or state properties. It is effective for concurrent protocols, hardware controllers, and finite-state software, but state explosion can require symmetry reduction, abstraction, or bounded analysis.
Abstract interpretation computes sound approximations of program behavior. It underlies many static analyzers: if the abstraction proves that an error state is unreachable, the corresponding claim is guaranteed within the analyzer's modeled semantics, although false alarms may remain.2
Verification succeeds only when the specification captures the intended property and the verification boundary is explicit. A proof of memory safety does not establish that an algorithm is useful, that a policy is fair, or that confidential information is never intentionally disclosed. Incorrect assumptions about hardware, libraries, undefined behavior, timing, or the compiler can also invalidate an otherwise correct argument.
Large projects commonly combine methods rather than seek one universal proof technique. Automated static analysis can screen broad codebases; model checking can examine concurrency protocols; deductive proofs can establish functional contracts; and tests can investigate requirements or environments that are difficult to model. Translation validation and verified compilation address another boundary by checking that generated code preserves properties of source programs.
The trusted computing base includes the proof kernel, specification language semantics, trusted libraries, and sometimes hardware models. Proof assistants reduce reliance on ad hoc tool output by checking proof objects with small kernels, but formalization still demands substantial design and maintenance effort.
Formal verification has reached production-scale components, not only classroom algorithms. The seL4 project reported a machine-checked functional-correctness proof for an operating-system microkernel, connecting an abstract specification to an implementation and making its assumptions explicit.3 The CompCert project likewise verified key correctness properties of a realistic optimizing C compiler, reducing the risk that compilation changes a verified program's meaning.4
Verification is also used for narrow, high-value claims rather than complete correctness. Examples include proving that cryptographic code avoids secret-dependent control flow, that a smart-contract state transition preserves an invariant, or that a driver obeys an interface protocol. Bounded model checking may find counterexamples without proving unbounded correctness; proof-carrying code and certified compilation instead attach machine-checkable evidence to software or transformations.
These examples show why “verified” is never a sufficient description by itself: the relevant question is which property, under which model, and across which implementation boundary.
Verification results should be read with their specification, semantics, assumptions, and trusted computing base; they do not automatically establish that software meets every informal human objective.
Help improve the encyclopedia. Reports go straight to the site manager.