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.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch