RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
about
|
people
|
publications
|
research
|
education
|
industry
|
conferences
|
media
|
projects
internal
description  |  members  |  activities  |  seminar  |  publications  |  software
  
search:
  

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