Formal methods

Se basa en

Requisitos previos obligatorios, hasta el fondo: 21

Aprenderás a

• 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.

Definición

• 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).

Teorema

• 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.

Errores frecuentes

• 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.

Descubrimientos opcionales

• ← Type theory and propositions as types
• ← Monads

Itinerarios de aprendizaje

• Computer science and formal methods

Lecturas complementarias

• 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)