On Implementing Unique Fixpoint Induction for Value-passing Processes

Huimin Lin

In TACAS, pages 104--118


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 symbol] BRICS WWW home page