<< A Chart Semantics for the Pi-Calculus | ホーム | JFlow: Practical Mostly-Static Information Flow Control >>

Proving Thread Termination

マルチスレッドなプログラムにおいてスレッドが停止するか示す方法。スレッドのインターリーブのすべての可能性を調べるのは非現実的なので、停止性を示したいスレッド以外を環境として抽象化してしまう。抽象化してしまうとシーケンシャルなプログラムの停止性の証明器が使える。反例が見つかれば潰すように環境を変更する。変更した環境が他のスレッドの抽象化として適切か調べて、不適切なら変更する。

author="Byron Cook and Andreas Podelski and Andrey Rybalchenko",
title="{Proving Thread Termination}",
booktitle="PLDI'07",
publisher="ACM Press",
volume="42",
pages="320--330",
year="2007"

タグ : ,
コメント追加 RSS feed for responses to this blog entry
投稿者 kw : 2007/07/17 16:10:13 JST #



コメント追加 トラックバック送信