Formal Methods in Computer Science
How to reason about computer programs and computing systems.
The term "formal methods" applies to all techniques that make computer
software and computing systems subject to reasoning. By treating computer
programs and system descriptions as language objects with a formal
semantics, we can think and argue about the behavior of the resulting
software and systems. The automatization of this process by supporting
software is currently a hot topic of research. Formal methods are
already industrially applied, e.g. to mission-critical software, computer chips,
or communication protocols.
The area includes the following topics:
- Specification
- To specify a system means to describe a behavior that
an implementation shall satisfy. There exist various
specification languages that allow to describe different aspects
of a system.
- Verification
- To verify a system means to show that it satisfies a
particular specification, to falsify means to show that it
violates the specification. This process can be automated by applying
automated theorem provers or model checkers.
- Transformation
- There exist various semantics-based techniques that allow to transform
a system into a "better" one. For
instance, partial evaluation takes a program and a program
argument and "compiles the argument into the program" to make it more efficient.
- Derivation/synthesis
- To derive or synthesize a program means to
automatically transform a specification into a program such that the
program satisfies the specification. This process usually proceeds in
multiple steps by making the specification more and more constructive.
See also the Wikipedia article, the organization Formal Methods Europe, the FM conference series,
and the RISC
research on Theorema.
Wolfgang Schreiner
Last modified: January 19, 2012
