Formal methods

Formal methods use mathematical languages and reasoning to specify system behavior and prove whether implementations satisfy stated properties.

Formal specification: A mathematically precise description of a system’s required behavior or constraints. Formal methods begin by expressing requirements in forms that can be analyzed.
Predicate logic: A logical system that represents objects, relations, and quantified statements. Formal specifications often express requirements with predicates and quantifiers.
seL4: A microkernel with a machine-checked proof of functional correctness and security properties. Its verification demonstrates formal methods applied to a production operating-system component.
Software testing: The execution of software under selected conditions to find defects or assess behavior. Testing samples executions, while formal verification can prove properties over defined models.
David Hilbert: A German mathematician whose program sought formal axiomatic foundations for mathematics. His formalist program helped shape the questions underlying rigorous verification.
Model checking: An automated technique that explores a finite-state model to determine whether it satisfies a property. It checks formal system models against properties such as safety and liveness.
Transition system: A mathematical model of states and the transitions between them. Many verification techniques represent system behavior as reachable state changes.
CompCert: A formally verified optimizing compiler for a large subset of the C programming language. Its correctness proof addresses risks introduced when translating source code into machine code.
Simulation: The use of an executable model to imitate a system’s behavior under chosen conditions. Simulation explores scenarios but does not by itself establish universal correctness.
Alan Turing: A British mathematician who defined abstract computation and made foundational contributions to logic. His work established mathematical models for computation that verification can analyze.

Linked from 6 pages