科研之友
微信
新浪微博
Facebook
分享链接
摘要
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.
- 出版日期2013
- 单位上海交通大学
