Overview

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Formal methods employ a variety of theoretical computer science fundamentals, including logic calculi, formal languages, automata theory, control theory, program semantics, type systems, and type theory.

History

Reasoning mathematically about programs predates the discipline's name. Alan Turing sketched a correctness argument for a routine in 1949, and in the late 1960s Robert W. Floyd and Tony Hoare established the axiomatic tradition of program proof that became Hoare logic. Edsger W. Dijkstra's weakest-precondition calculus gave a systematic way to derive programs from specifications, and model-oriented specification languages such as VDM and the Z notation were developed during the 1970s.

A second tradition grew out of temporal logic. Amir Pnueli proposed it in 1977 as a language for specifying the behaviour of reactive programs, and model checking was introduced independently by Edmund M. Clarke and E. Allen Emerson and by Jean-Pierre Queille and Joseph Sifakis in the early 1980s, work for which the three shared the 2007 Turing Award. Symbolic model checking with binary decision diagrams raised the size of systems that could be analysed by orders of magnitude, and bounded model checking built on SAT solvers extended it further.

Industrial interest was sharpened by costly defects such as the 1994 Pentium FDIV bug, which prompted processor vendors to invest heavily in hardware verification. From the 2000s onwards, maturing SMT solvers and proof assistants made it practical to verify complete systems rather than isolated components.

Uses

Formal methods can be applied at various points through the development process.

Specification

Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system.

Alternatively, specification may be the only stage in which formal methods are used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.

The need for formal specification systems has been noted for years. In the ALGOL 58 report, John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus–Naur form (BNF). Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.

Synthesis

Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.