Science

Since the 1930s mathematical logicians have studied computational processes as mathematical objects. Since the 1950s computer scientists have studied computational processes and the programs that represent them. Basic research in these areas has included

relations between proofs of existence of objects and programs for computing them
formalisms for specifying computers and parts of computers
formalisms for specifying computer programs, i.e. saying what a program should accomplish
mathematical proofs that programs meet their specifications
logics of computational processes
computer programs for verifying mathematical proofs - especially proofs that programs meet their specifications
computer programs for going from the specifications of programs and hardware automatically to programs and hardware designs that meet the specifications
computer programs for constructing mathematical proofs, especially proofs of program correctness

Technology

On the basis of this science and mathematics, a technology has gradually developed for increasing the reliability of hardware and software by

verifying that they meet their specifications
- either by human-checked proofs
- or by human generated machine checked proofs
- interactive verification involving humans and machines
- automatic machine verification
systems for interactively going from the specifications to programs and hardware that meet them.

Present State of the Art

Here goes a list of a few exemplary applications -- Boyer and Moore (CLINC), Rushby , ORA ...

Some WWW pages related to Formal Methods

A Database of Automated Reasoning Systmes maintained by Carolyn Talcott.

A Formal Methods Page maintained by Jonathon Bowen.

Future Directions

Application developers and software engineers must deal with complex software systems, not just single isolate programs. They are often distributed, and composed of heterogeneous parts. They evolve over time, and must function in environment over which they have no control. New formal methods are needed to address problems of scaling, provide the ability to use partial information, and combine methods based on widely varying formalism, addressing different aspects of specification and analysis.