Towards a Semantic-Based Verification Environment for the pi-calculus
π計算のインタプリタと双模倣関係の判定器のプロトタイプを作ったという論文。π計算は名前の代入があって操作的意味論がCCSみたいな「普通」のLTSでは表せなくて、既存のツールが再利用できない。そこで「普通」のLTSで意味論が表せるπ計算の変種を定義して、それをJACKという既存のツール上に実現したらしい。π計算の変種の話は別の論文読んだほうがいいかな。
author="Gianluigi Ferrari and Gianfranco Modoni and Paola Quaglia",
title="{Towards a Semantic-Based Verification Environment for the $\pi$-calculus}",
booktitle="5th Italian Conference on Theoretical Computer Science",
pages="451--465",
year="1995"