4 min read
On this page

Program Verification

Overview

Verification Spectrum from Testing to Theorem Proving

Program verification proves that code meets its specification. Unlike testing (which checks specific inputs), verification provides guarantees about all possible executions. The foundational framework is Hoare logic, which reasons about programs using logical assertions.

Hoare Logic

Hoare Triples

A Hoare triple {P} S {Q} states: if precondition P holds before executing statement S, then postcondition Q holds after S terminates.

  • Partial correctness {P} S {Q}: if S terminates, Q holds (says nothing about termination)
  • Total correctness [P] S [Q]: S terminates AND Q holds

Axioms and Rules

Assignment axiom:

{Q[x/E]} x := E {Q}

Read backwards: to establish Q after assigning E to x, require Q with x replaced by E before.

Sequence rule:

{P} S1 {R}    {R} S2 {Q}
─────────────────────────
     {P} S1; S2 {Q}

Conditional rule:

{P ∧ B} S1 {Q}    {P ∧ ¬B} S2 {Q}
────────────────────────────────────
     {P} if B then S1 else S2 {Q}

While rule (partial correctness):

{I ∧ B} S {I}
──────────────────────
{I} while B do S {I ∧ ¬B}

I is the loop invariant: true before the loop, preserved by each iteration, and combined with loop exit condition to establish the postcondition.

Consequence rule (strengthening pre, weakening post):

P' → P    {P} S {Q}    Q → Q'
──────────────────────────────
        {P'} S {Q'}

Total Correctness for Loops

For total correctness, add a variant (termination measure): a well-founded expression that decreases with each iteration.

{I ∧ B ∧ V = v} S {I ∧ V < v}    V ≥ 0 when I ∧ B
────────────────────────────────────────────────────
         [I] while B do S [I ∧ ¬B]

Weakest Precondition

The weakest precondition wp(S, Q) is the weakest condition P such that {P} S {Q}. Dijkstra's predicate transformer semantics computes wp mechanically:

wp(x := E, Q)                = Q[x/E]
wp(S1; S2, Q)                = wp(S1, wp(S2, Q))
wp(if B then S1 else S2, Q)  = (B → wp(S1,Q)) ∧ (¬B → wp(S2,Q))
wp(skip, Q)                  = Q

For loops, wp cannot be computed automatically -- the loop invariant must be supplied.

Verification Condition Generation (VCG)

Given annotated code (with loop invariants and pre/post conditions), a VCG tool automatically generates verification conditions (VCs) -- logical formulas that, if valid, guarantee correctness.

Pipeline:  Annotated Program → VCG → VCs → SMT Solver → ✓ or counterexample

VCs are typically discharged by SMT solvers (Z3, CVC5) that handle combinations of theories (arithmetic, arrays, bit-vectors, etc.).

Loop Invariants

Finding loop invariants is the main creative challenge in program verification.

Example: binary search

// Pre: sorted(a) ∧ 0 ≤ lo ≤ hi ≤ len(a)
while lo < hi {
    // Invariant: 0 ≤ lo ≤ hi ≤ len(a)
    //          ∧ ∀i. 0 ≤ i < lo → a[i] < target
    //          ∧ ∀i. hi ≤ i < len(a) → a[i] ≥ target
    mid := (lo + hi) / 2
    if a[mid] < target { lo = mid + 1 }
    else { hi = mid }
}
// Post: (lo < len(a) ∧ a[lo] = target) ∨ target not in a

Properties of a good loop invariant:

  1. True on loop entry (initialization)
  2. Preserved by each iteration (maintenance)
  3. Together with loop exit condition, implies the postcondition (termination/usefulness)
  4. Weak enough to be provably maintained
  5. Strong enough to prove the postcondition

Automated invariant inference: abstract interpretation, predicate abstraction, and machine learning techniques can infer invariants automatically for many practical loops.

Verification Tools

Dafny

A verification-aware programming language developed at Microsoft Research. Programs include specifications that are checked at compile time via Z3.

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= index < a.Length ==> a[index] == key
  ensures index == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant forall i :: 0 <= i < lo ==> a[i] < key
    invariant forall i :: hi <= i < a.Length ==> a[i] > key
    decreases hi - lo
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key { lo := mid + 1; }
    else if a[mid] > key { hi := mid; }
    else { return mid; }
  }
  return -1;
}

Features: ghost variables, lemmas as methods, algebraic datatypes, termination checking, refinement, concurrent reasoning via dynamic frames.

SPARK Ada

A formally verifiable subset of Ada used in high-assurance systems (avionics, rail, defense).

procedure Increment (X : in out Integer)
  with Pre  => X < Integer'Last,
       Post => X = X'Old + 1
is
begin
   X := X + 1;
end Increment;
  • SPARK tools generate VCs discharged by CVC5/Z3/Alt-Ergo
  • Flow analysis checks information flow and absence of uninitialized variables
  • Used in production: NVIDIA GPU firmware, Thales air traffic control, GNAT runtime

Frama-C

A platform for analysis of C code. ACSL (ANSI/ISO C Specification Language) annotations express specifications.

/*@ requires \valid(a+(0..n-1));
    requires n > 0;
    ensures \result >= 0 && \result < n;
    ensures \forall integer i; 0 <= i < n ==> a[\result] <= a[i];
*/
int find_min(int *a, int n) {
    int min_idx = 0;
    /*@ loop invariant 1 <= i <= n;
        loop invariant 0 <= min_idx < n;
        loop invariant \forall integer j; 0 <= j < i ==> a[min_idx] <= a[j];
        loop variant n - i;
    */
    for (int i = 1; i < n; i++) {
        if (a[i] < a[min_idx]) min_idx = i;
    }
    return min_idx;
}
  • WP plugin: weakest-precondition-based deductive verification
  • EVA plugin: abstract interpretation for runtime error detection
  • Integrates with multiple provers via Why3

Separation Logic

Separation logic extends Hoare logic to reason about pointer-manipulating programs and heap-allocated data.

Core Connectives

| Connective | Meaning | |------------|---------| | emp | Heap is empty | | x ↦ v | x points to value v (and nothing else) | | P * Q | Separating conjunction: P and Q hold on disjoint heap regions | | P -* Q | Magic wand: if P is added to the current heap, Q holds |

The Frame Rule

    {P} S {Q}
─────────────────
{P * R} S {Q * R}

If S operates only on the heap described by P, then any disjoint frame R is preserved. This enables local reasoning: verify each function considering only the memory it touches.

Example

// Specification for list append
{list(x, xs) * list(y, ys)}
  append(x, y)
{list(x, xs ++ ys)}

The * ensures x and y point to disjoint lists. After append, the combined list is at x.

Separation logic tools: VeriFast, Viper, Gillian, Facebook Infer (for bug finding at scale using bi-abduction).

Comparison of Approaches

| Tool/Method | Language | Automation | Domain | |-------------|----------|------------|--------| | Dafny | Dafny | High (Z3) | General purpose | | SPARK | Ada subset | High | Safety-critical | | Frama-C | C (ACSL) | Moderate | Systems code | | VeriFast | C, Java | Moderate | Pointer programs | | Viper | Viper IL | High | Heap programs |

Key Takeaways

  • Hoare logic provides the theoretical foundation: pre/post conditions + inference rules
  • Weakest precondition calculus enables mechanical generation of verification conditions
  • Loop invariants are the key intellectual challenge -- they encode "why the loop works"
  • Modern tools (Dafny, SPARK, Frama-C) make verification practical for real software
  • Separation logic's frame rule enables modular reasoning about heap-manipulating code
  • SMT solvers are the workhorse backend, automating the discharge of proof obligations