On Implementing Unique Fixpoint Induction for Value-passing Processes
In TACAS, pages
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.
Chinese Academy of Sciences, Beijing, China.
Available as PostScript.
BRICS WWW home page