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 language | English |
|---|---|
| Pages (from-to) | 1504-1513 |
| Number of pages | 10 |
| Journal | Journal of Networks |
| Volume | 8 |
| Issue number | 7 |
| DOIs | |
| Publication status | Published - 2013 |
| Externally published | Yes |
Keywords
- Symbolic bisimulation
- Value-passing calculus
- Verification