Model checking Erlang programs – LTL-propositions and abstract interpretation

Abstract

We present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. In previous work we defined a framework for the verification of Erlang programs using abstract interpretation and LTL model checking. The application of LTL model checking yields some problems in the verification of state propositions, because propositions are also abstracted in the framework. While state propositions must be satisfied, negated state propositions have to be refuted. We show how this can be decided by means of the abstract domain. The approach is implemented as a prototype and we are able to prove properties like mutual exclusion or the absence of deadlocks and lifelocks for some Erlang programs.