5th International Workshop on
Formal Methods for Industrial Critical Systems
Berlin, April 3-4, 2000
Verification of Erlang Programs:
Factoring out the Side-effect-free Fragment
Erlang is a functional programming language developed at Ericsson
for writing economical and yet powerful and ecient telecommunication
applications. Correctness is of major importance in such applications,
and since they usually exhibit a high degree of concurrency, testing is
often not sufficient. Verification, namely formally proving that a system
is correct, is becomming a more and more widespread practice. Due to
the complexity ofErlang, there is no general method for verification of
arbitrary Erlang programs, which is e ective and at the same time leads
to economic proofs. However, one can do much better in specialised cases
which are well-understood. A main direction of research is the identification of fragments of Erlang for which eficient verification methods exist.
One such fragment is the side-effect-free one, in which an Erlang expression is evaluated purely for its value, and is not affecting the environment
in which it is evaluated in terms of sending messages, reading from the
message queue, or process spawning. This is furthermore a very common
situation, given the number of libraries of side-effect-free functions used
extensively in practice. The present paper is dedicated to reasoning about
the behaviour of an Erlang system modulo replacement of side-effect-free
Erlang expressions with the result of their evaluation. The proposed approach fits at the same time the compositional reasoning paradigm used
for reasoning about large component-based software.
Note: The content of the following files is part of
GMD Report No. 91
and subject to its copyright.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch