This group gathers pioneers of software and its engineering whose primary contribution was proving software or hardware correct through mathematical logic, including model checking, theorem proving, abstract interpretation, type theory, denotational and operational semantics, and specification languages such as Z, VDM and B. It follows the Formal Methods second-level heading of the ACM Computing Classification System under Software and its engineering. Their shared work is establishing, with mathematical rigor, that a system meets its specification, as distinct from writing the system code, its compiler or its process documentation.