Skip to content
The Lumenary
First-year graduateComputationPlanned

Formal methods

Mathematical methods for specifying and verifying software and hardware: operational and denotational semantics, Hoare logic, model checking, type soundness, and proof assistants for verified programs.

math.comp.formal-methods

Show everything needed to reach this topic

The lesson for this topic has not been written yet. The outline below is part of the curriculum map and has not been reviewed.

Builds on

First-order logicThe λ-calculusAlgorithm design and analysis

Required prerequisites, all the way down: 21

You will learn to

  • Give an operational semantics for a small imperative language and prove properties by induction on derivations.
  • Verify programs with Hoare triples and loop invariants.
  • Model-check finite-state systems against temporal-logic specifications.

Definition

  • A Hoare triple {P} C {Q} asserts that if P holds before command C runs and C terminates, then Q holds afterwards.
  • Model checking algorithmically decides whether a finite model satisfies a temporal-logic formula.
  • A type system is sound if well-typed programs cannot reach a stuck state (progress and preservation).

Theorem

  • Hoare logic is sound, and it is relatively complete for suitable languages (Cook).
  • CTL model checking can be done in time linear in the product of the sizes of the model and the formula.
  • By Rice's theorem, verifying arbitrary properties of arbitrary programs cannot be fully automated.

Common misconceptions

  • Thinking a verified program is correct in every sense; it is correct relative to its specification and its trusted base.
  • Believing partial correctness implies termination.

Optional discoveries

Learning pathways

Further reading

  • Glynn Winskel, The Formal Semantics of Programming Languages (1993)
  • Michael Huth and Mark Ryan, Logic in Computer Science
  • Christel Baier and Joost-Pieter Katoen, Principles of Model Checking (2008)