研究生一年级Computation计划中

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

显示到达此主题所需的全部内容

本主题的课程尚未编写。下面的提纲是课程地图的一部分，尚未经过审校。

前置知识

First-order logic The λ-calculus Algorithm design and analysis

21 项必需的前置知识（一直追溯到底）

你将学会

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.

定义

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

定理

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.

常见误解

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.

可选发现

← Type theory and propositions as types
← Monads

学习路径

Computer science and formal methods