In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems.
Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system.
[6] 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."
Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.
In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means.
Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified.
The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned.
Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators[9] to get fast convergence.
expresses that an execution of a program conforms to the specification, a binary decision diagram can be used to determine if
[13] Formal methods are applied in different areas of hardware and software, including routers, Ethernet switches, routing protocols, security applications, and operating system microkernels such as seL4.
Dansk Datamatik Center used formal methods in the 1980s to develop a compiler system for the Ada programming language that went on to become a long-lived commercial product.
For sequential software, examples of formal methods include the B-Method, the specification languages used in automated theorem proving, RAISE, and the Z notation.
Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of first-order logic—and then to directly execute the logic as though it were a program.
A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.
[27][28] They contend that the expressiveness of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task.
As an alternative, various lightweight formal methods, which emphasize partial specification and focused application, have been proposed.
For example, the Boolean satisfiability problem is NP-complete by the Cook–Levin theorem, but SAT solvers can solve a variety of large instances.