Abstract
Erlang is a functional programming language developed by Ericsson Telecom which is particularly well suited for implementing con- current 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 termi- nation 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 two refinements of this technique, viz. narrowing and rewriting dependency pairs. These refinements are not only of use in the industrial application sketched in this paper, but they are generally applicable to arbitrary (C)TRSs. Thus, in this way dependency pairs can be used to prove ter- mination of even more (C)TRSs automatically.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
T. Arts & M. Dam, Verifying a distributed database lookup manager written in Erlang. In Proc. FM’ 99, Toulouse, France, 1999.
T. Arts & J. Giesl, Automatically proving termination where simplification orderings fail. TAPSOFT’ 97, LNCS 1214, pp. 261–273, Lille, France, 1997.
T. Arts & J. Giesl, Proving innermost normalisation automatically. In Proc. RTA-97, LNCS 1232, pp. 157–172, Sitges, Spain, 1997.
T. Arts & J. Giesl, Modularity of termination using dependency pairs. In Proc. RTA-98, LNCS 1232, pp. 226–240, Tsukuba, Japan, 1998.
T. Arts & J. Giesl, Termination of term rewriting using dependency pairs. TCS. To appear. Preliminary version under http://www.inferenzsysteme.informatik.tu-darmstadt.de/~reports/notes/ibn-97–46.ps
F. Baader & T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
J. A. Bergstra & J. W. Klop, Conditional rewrite rules: confluence and termination. JCSS, 32:323–362, 1986.
H. Bertling & H. Ganzinger, Completion-time optimization of rewrite-time goal solving. Proc. RTA-89, LNCS 355, pp. 45–58, Chapel Hill, USA, 1989.
N. Dershowitz & D. A. Plaisted, Equational programming. Machine Intelligence, 11:21–56, Oxford University Press, 1987.
N. Dershowitz, Termination of rewriting. JSC, 3:69–116, 1987.
N. Dershowitz, M. Okada, & G. Sivakumar, Canonical conditional rewrite systems. In Proc. CADE-9, LNCS 310, pp. 538–549, Argonne, USA, 1988.
N. Dershowitz & M. Okada, A rationale for conditional equational programming. TCS, 75:111–138, 1990.
N. Dershowitz & J.-P. Jouannaud, Rewrite Systems. In Handbook of Theoretical Computer Science, Vol. B, pp. 243–320, Elsevier, 1990.
N. Dershowitz & C. Hoot, Natural termination. TCS, 142(2):179–207, 1995.
M. J. Fay, First-order unification in an equational theory. Proc. 4th Workshop on Automated Deduction, pp. 161–167, Austin, TX, Academic Press, 1979.
E. Giovanetti & C. Moiso, Notes on the eliminations of conditions. In Proc. CTRS’ 87, LNCS 308, pp. 91–97, Orsay, France, 1987.
B. Gramlich, On termination and confluence of conditional rewrite systems. In Proc. CTRS’ 94, LNCS 968, pp. 166–185, Jerusalem, Israel, 1994.
B. Gramlich, Abstract relations between restricted termination and confluence properties of rewrite systems. Fundamenta Informaticae, 24:3–23, 1995.
B. Gramlich, Termination and confluence properties of structured rewrite systems. PhD Thesis, Universität Kaiserslautern, Germany, 1996.
B. Gramlich, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems. TCS, 165:97–131, 1996.
M. Hanus, The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19,20:583–628, 1994.
Patent pending, Ericsson Telecom AB, 1999.
S. Kaplan, Conditional rewrite rules. TCS, 33:175–193, 1984.
M. Marchiori, Unravelings and Ultra-properties, Proc. ALP’ 96, LNCS 1139, pp. 107–121, Aachen, Germany, 1996.
A. Middeldorp, Modular properties of conditional term rewriting systems. Information and Computation, 104:110–158, 1993.
J. Steinbach, Simplification orderings: history of results. Fundamenta Informaticae, 24:47–87, 1995.
T. Suzuki, A. Middeldorp, & T. Ida, Level-confluence of conditional rewrite systems with extra variables in right-hand sides. Proc. RTA-95, LNCS 914, pp. 179–193, Kaiserslautern, Germany, 1995.
C.-P. Wirth & B. Gramlich, A constructor-based approach for positive/negative conditional equational specifications. JSC, 17:51–90, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arts, T., Giesl, J. (1999). Applying Rewriting Techniques to the Verification of Erlang Processes. In: Flum, J., Rodriguez-Artalejo, M. (eds) Computer Science Logic. CSL 1999. Lecture Notes in Computer Science, vol 1683. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48168-0_8
Download citation
DOI: https://doi.org/10.1007/3-540-48168-0_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66536-6
Online ISBN: 978-3-540-48168-3
eBook Packages: Springer Book Archive