Collection

Tag: formal-specification

PVS and the Integration of Specification with Interactive Proof

PVS integrated a rich higher-order specification language, type checking, automated decision procedures, and interactive theorem proving into one environment for serious formal verification.

↗

Jean-Raymond Abrial, Z, and the Rise of Formal Specification Before Implementation

Z made abstract state, invariants and operations into a mathematical specification language, while Abrial's later B work pushed formal methods toward refinement and verified construction.

↗