Verification of Erlang Processes by Dependency Pairs |
| |
Authors: | Jürgen Giesl Thomas Arts |
| |
Affiliation: | LuFG Informatik II, RWTH Aachen, Ahornstrasse 55, 52074 Aachen, Germany (e-mail: giesl@informatik.rwth-aachen.de), DE Computer Science Lab., Ericsson Utvecklings AB, Box 1505, 125 25 ?lvsj?, Sweden (e-mail: thomas@cslab.ericsson.se), SE
|
| |
Abstract: | 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 presently used at Ericsson. To
verify properties of processes, such a property is transformed into a termination problem of a conditional term rewriting
system (CTRS). Subsequently, this termination proof can be performed automatically using dependency pairs.
The paper illustrates how the dependency pair technique can be applied for termination proofs of conditional TRSs. Secondly, we present three refinements of this technique, viz. narrowing, rewriting, and instantiating dependency pairs. These refinements are not only of use in the industrial applications sketched in this paper, but they are generally applicable
to arbitrary (C)TRSs. Thus, in this way dependency pairs can be used to prove termination of even more (C)TRSs automatically.
Received: October 6, 1999 |
| |
Keywords: | : Verification Distributed processes Rewriting Termination |
本文献已被 SpringerLink 等数据库收录! |
|