Model Checking Erlang Programs -- Abstracting the Context-Free Structure
In Proc. of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001)
, Report No. 2017, University of Kiel
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
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
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
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.