情報流解析に基づくリファクタリングの提案。機密データを扱うコンポーネントを分離し、境界を越えるところで declassify する。論文では例とリファクタリングする際に問題となる点に対して考察が行われているだけで、具体的なリファクタリングの定義などは何もなし。

author="Scott F. Smith and Mark Thober",
title="{Refactoring Programs to Secure Information Flows}",
booktitle="PLAS 2006",
publisher="ACM Press",
pages="75--84",
year="2006"

コメント追加

投稿者 kw : 2007/07/23 11:03:45 JST #

Javaの機能を極力削らないようにしながら情報流解析を導入して拡張した言語JFlowの論文。型システムとかの詳細は省かれていて、言語の解説がほとんど。Jifという後継(?)がある。

author="Andrew C.Myers",
title="{JFlow: Practical Mostly-Static Information Flow Control}",
booktitle="POPL'99",
publisher="ACM Press",
pages="228--241",
year="1999"

コメント追加

投稿者 kw : 2007/07/17 18:05:29 JST #

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

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"

コメント追加

投稿者 kw : 2007/07/17 16:10:13 JST #

π計算の意味論を図的に定義しようという論文。実行系列の図的表現ではなく、図を使って意味を定義しているところが新しい。垂直方向にプロセスの状態、水平方向にメッセージ通信を記述する。数式表現に比べれば直観的にわかりやすいことと、履歴が一緒に表現されることが利点として主張されている。Chart Semantics と通常の Reduction Semantics の関係についても議論している。

author="Johannes Borgstroem and Andrew D. Gordon and Andrew Phillips",
title="{A Chart Semantics for the Pi-Calculus}",
booktitle="EXPRESS 2007",
year="2007"

コメント追加

投稿者 kw : 2007/07/15 18:44:19 JST #