An interpretation of Erlang into value-passing Calculus

H. Huang, F. Yang

Research output: Contribution to journalArticleAcademicpeer-review

127 Downloads (Pure)

Abstract

In this paper we present a new process calculus VPCΣ and an interpretation for core Erlang. VPCΣ is at least as expressive as VPC and it is more effective for verification with some built-in functions. The wellestablished symbolic bisimulation in value-passing calculus is now helpful for solving the infinite-state space problem of data values in equivalence checking and verfication. Compared to the previous formalization work of modeling core Erlang in π-calculus, the new interpretation has the following main merits: some essential features for Erlang are implemented faithfully; and above all the soundness of the interpretation is proved with respect to late symbolic bisimulation.

Original languageEnglish
Pages (from-to)1504-1513
Number of pages10
JournalJournal of Networks
Volume8
Issue number7
DOIs
Publication statusPublished - 2013
Externally publishedYes

Keywords

  • Symbolic bisimulation
  • Value-passing calculus
  • Verification

Cite this