On Implementing Unique Fixpoint Induction for Value-passing Processes
Huimin Lin
In TACAS, pages
104--118
Abstract:
We examine the possible pitfalls in formulating the unique
fixpoint induction proof rule in the setting of value-passing process calculi
and describe how this rule is implemented in the verification tool
VPAM. An argument is also given to justify the implementation.
Comments
Chinese Academy of Sciences, Beijing, China.
Available as PostScript.
BRICS WWW home page