Model Checking Erlang Programs -- Abstracting the Context-Free Structure

Frank Huch

In Proc. of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001) , Report No. 2017, University of Kiel

Abstract

We present an approach for the verification of Erlang programs using abstract interpretation and model checking. In general model checking for temporal logics and Erlang programs is undecidable. Therefore we defined a framework for abstract interpretations for Erlang. In this framework it is guaranteed, that the abstract operational semantics preserves all paths of the standard operational semantics. We consider properties that have to hold on all paths of a system, like properties in LTL. If these properties can be proven for the abstract operational semantics, they also hold for the Erlang program. The prove can be automated with model checking if the abstract operational semantics is a finite transition system. But finiteness cannot be guaranteed because of the context-free structure of functional programming languages. Even for finite domain abstract interpretations we get infinite state systems and model checking is undecideable. The reduction terms can grow infinitely in non-tail recursive calls. In this paper we define an abstraction of the context-free structure of Erlang programs. It replaces the recursive calls in non-tail positions by jumps to the last call of the same function. The corresponding returns are replace by jumps to the possible return points. We have implemented this approach as a prototype and are able to prove properties like mutual exclusion or the absence of deadlocks and lifelocks for some Erlang programs.