Computer Science › Intelligence + Theory
Testing can find concrete failures, but formal verification asks for a mathematical argument that every behavior allowed by the model satisfies a specification. This frames the discipline by connecting software testing to logic and to the Halting Problem limits already proved in Computability and Complexity.
A verifier cannot prove “the program is good” until “good” is written as predicates over the states before, after, and during execution. Preconditions, postconditions, and invariants turn informal intent into objects Hoare logic and model checking can manipulate.
Formal specifications are built from the connectives, predicates, and quantifiers introduced in Discrete Math and Logic. The new step is interpreting those formulas over program states, heaps, arrays, and traces.
The Hoare triple `{P} C {Q}` is the central judgment of axiomatic program verification: if command C starts in a state satisfying P and terminates, it ends in a state satisfying Q. It separates specification from implementation while staying tied to operational semantics.
Hoare logic becomes useful because triples can be derived compositionally: assignment, sequencing, conditionals, loops, and consequence each have local rules. These rules let a proof follow the structure of the program instead of enumerating executions.
A loop invariant is the assertion that makes unbounded repetition finite enough to reason about. The while rule turns initialization, preservation, and exit reasoning into a proof for every number of iterations.
Weakest preconditions run a specification backward through code: given a desired postcondition, compute the least restrictive condition that must hold before the command. This turns proof search into calculational verification-condition generation.
Total correctness strengthens partial correctness by also proving termination. Variants and ranking functions connect program loops to well-founded descent, while the Halting Problem explains why no automatic method can always find them.
SAT asks whether a Boolean formula has any satisfying assignment, and Cook-Levin explains why that problem is a universal meeting point for efficient verification. Formal tools exploit SAT by reducing finite proof obligations and bounded executions to Boolean search.
SMT extends SAT with background theories such as integers, arrays, bit-vectors, and uninterpreted functions. Decision procedures make many verification conditions automatic while preserving the boundary between decidable fragments and general program behavior.
Model checking begins by replacing a program or protocol with a finite graph of states and transitions. A Kripke structure adds atomic propositions to states so temporal-logic formulas can be evaluated over executions.
LTL describes properties of individual execution paths using operators such as □, ◇, ○, and 𝖴. It is the natural language for saying that bad things never happen and good things eventually happen along a run.
CTL adds explicit path quantifiers, separating what must hold on all possible futures from what may hold on at least one future. Branching time is especially useful when nondeterminism represents scheduling, environment choices, or underspecified components.
Explicit-state model checking explores all reachable states of a finite model and reports either that a temporal property holds or that a counterexample trace exists. This is proof by exhaustive graph search, automated where the state space is finite enough.
State-space explosion is the central engineering obstacle in model checking: variables, components, and interleavings multiply reachable states. Symbolic model checking, abstraction, partial-order reduction, and BDDs attack that explosion by representing sets of states compactly.
Proof assistants turn mathematical proofs into checkable artifacts, often using the Curry-Howard correspondence between propositions and types. They complement automation by letting humans supply invariants, lemmas, and structure that solvers cannot discover reliably.
Formal verification is limited not by lack of ambition but by precise theorems: the Halting Problem and Rice’s Theorem rule out a complete automatic verifier for nontrivial semantic properties of arbitrary programs. Sound tools remain valuable by making their assumptions and scope explicit.
The capstone verifies one small program both deductively and by finite-state exploration. Seeing the same requirement as a Hoare proof and as a model-checking property makes the tradeoff between symbolic reasoning and exhaustive search concrete.
Part of the Computer Science curriculum.
Testing can find concrete failures, but formal verification asks for a mathematical argument that every behavior allowed by the model satisfies a specification. This frames the discipline by connecting software testing to logic and to the Halting Problem limits already proved in Computability and Complexity.
A verifier cannot prove “the program is good” until “good” is written as predicates over the states before, after, and during execution. Preconditions, postconditions, and invariants turn informal intent into objects Hoare logic and model checking can manipulate.
Formal specifications are built from the connectives, predicates, and quantifiers introduced in Discrete Math and Logic. The new step is interpreting those formulas over program states, heaps, arrays, and traces.
The Hoare triple `{P} C {Q}` is the central judgment of axiomatic program verification: if command C starts in a state satisfying P and terminates, it ends in a state satisfying Q. It separates specification from implementation while staying tied to operational semantics.
Hoare logic becomes useful because triples can be derived compositionally: assignment, sequencing, conditionals, loops, and consequence each have local rules. These rules let a proof follow the structure of the program instead of enumerating executions.
A loop invariant is the assertion that makes unbounded repetition finite enough to reason about. The while rule turns initialization, preservation, and exit reasoning into a proof for every number of iterations.
Weakest preconditions run a specification backward through code: given a desired postcondition, compute the least restrictive condition that must hold before the command. This turns proof search into calculational verification-condition generation.
Total correctness strengthens partial correctness by also proving termination. Variants and ranking functions connect program loops to well-founded descent, while the Halting Problem explains why no automatic method can always find them.
SAT asks whether a Boolean formula has any satisfying assignment, and Cook-Levin explains why that problem is a universal meeting point for efficient verification. Formal tools exploit SAT by reducing finite proof obligations and bounded executions to Boolean search.
SMT extends SAT with background theories such as integers, arrays, bit-vectors, and uninterpreted functions. Decision procedures make many verification conditions automatic while preserving the boundary between decidable fragments and general program behavior.
Model checking begins by replacing a program or protocol with a finite graph of states and transitions. A Kripke structure adds atomic propositions to states so temporal-logic formulas can be evaluated over executions.
LTL describes properties of individual execution paths using operators such as □, ◇, ○, and 𝖴. It is the natural language for saying that bad things never happen and good things eventually happen along a run.
CTL adds explicit path quantifiers, separating what must hold on all possible futures from what may hold on at least one future. Branching time is especially useful when nondeterminism represents scheduling, environment choices, or underspecified components.
Explicit-state model checking explores all reachable states of a finite model and reports either that a temporal property holds or that a counterexample trace exists. This is proof by exhaustive graph search, automated where the state space is finite enough.
State-space explosion is the central engineering obstacle in model checking: variables, components, and interleavings multiply reachable states. Symbolic model checking, abstraction, partial-order reduction, and BDDs attack that explosion by representing sets of states compactly.
Proof assistants turn mathematical proofs into checkable artifacts, often using the Curry-Howard correspondence between propositions and types. They complement automation by letting humans supply invariants, lemmas, and structure that solvers cannot discover reliably.
Formal verification is limited not by lack of ambition but by precise theorems: the Halting Problem and Rice’s Theorem rule out a complete automatic verifier for nontrivial semantic properties of arbitrary programs. Sound tools remain valuable by making their assumptions and scope explicit.
The capstone verifies one small program both deductively and by finite-state exploration. Seeing the same requirement as a Hoare proof and as a model-checking property makes the tradeoff between symbolic reasoning and exhaustive search concrete.