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