Verification of Erlang processes by dependency pairs

Erlang is a functional programming language developed by Ericsson Telecom, which is particularly well suited for implementing concurrent processes. In this paper we show how methods from the area of term rewriting are present ly used at Ericsson. To verify properties of processes, such a property is transformed into a termination problem of a conditional term rewriting syst em (CTRS). Subsequently, this termination proof can be performed automatica lly using dependency pairs. The paper illustrates how the dependency pair technique can be applied for termination proofs of conditional TRSs. Secondly, we present three refineme nts of this technique, viz. narrowing, rewriting, and instantiating depende ncy pairs. These refinements are not only of use in the industrial applicat ions sketched in this paper, but they are generally applicable to arbitrary (C)TRSs. Thus, in this way dependency pairs can be used to prove terminati on of even more (C)TRSs automatically.