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"
A Chart Semantics for the Pi-Calculus
π計算の意味論を図的に定義しようという論文。実行系列の図的表現ではなく、図を使って意味を定義しているところが新しい。垂直方向にプロセスの状態、水平方向にメッセージ通信を記述する。数式表現に比べれば直観的にわかりやすいことと、履歴が一緒に表現されることが利点として主張されている。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"
Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes
π計算のプロセスの spatial property について partial order reduction する話。partial order reduction が可能な論理式のクラスを明らかにしている。
author="Reynald Affeldt and Naoki Kobayashi",
title="{Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes}",
booktitle="EXPRESS 2004",
publisher="Elsevier",
volume="128",
series="ENTCS",
pages="151--168",
year="2005"
Detecting Structural Refactoring Conflicts Using Critical Pair Analysis
複数のリファクタリング操作を行おうとしている時に、それらの操作が衝突していないか検出する手法を提案している論文。検出は、操作をグラフ変換を用いて表し、危険対を求めるアルゴリズムを利用する。論文にはいくつかのリファクタリング操作について結果だけ示してあり、例えば「メソッドの移動」と「変数のカプセル化」が衝突する。また、適用する順序によって衝突したりしなかったりするペアも示されている。また、衝突するそれぞれの操作を適用した後で別の操作により合流することができかどうかの考察も行っている。
author="Tom Mens and Gabriele Taentzer and Olga Runge",
title="{Detecting Structural Refactoring Conflicts Using Critical Pair Analysis}",
booktitle="Proceedings of the Workshop on Software Evolution through Transformations: Model-based vs. Implementation-level Solutions",
publisher="Elsevier",
volume="127",
series="ENTCS",
pages="113--128",
year="2005"
A Unifying Framework for Process Calculus Semantics of Concurrent Object-Oriented Languages
並行オブジェクト指向言語の意味論を CCS で定義した論文。似たようなことをやった研究は他にもあるけど、継承まで考慮に入れているのは他では見たことはないはず。コーディング方法としてはわりと普通。
author="Michael Papathomas",
title="{A Unifying Framework for Process Calculus Semantics of Concurrent Object-Oriented Languages}",
booktitle="Object-Oriented Concurrent Computing",
publisher="Springer",
volume="612",
series="LNCS",
pages="53--79",
year="1992"
An Extensible Meta-Model for Program Analysis
Cross-Language Program Analysis and Refactoring と同時期に出た論文。いろいろなプログラミング言語に共通するモデルを作るための枠組みの話。実際にどのようにモデルを作るかといった具体的なことはほとんど載ってない。モデルは基本的に木構造で、ノードの集合、木構造の定義、ルートノード、ノード間の関係から定義される。言語固有のモデルも共通モデルも同じで、あとは固有モデルから共通モデルへのマッピングを定義する。ということで、よく考えると特に変わったことを言ってるわけではない感じ。
author="Dennis Strein and R{\"u}diger Lincke and Jonas Lundberg and Welf L{\"o}we",
title="{An Extensible Meta-Model for Program Analysis}",
booktitle="ICSM '06",
publisher="IEEE Press",
pages="380--390",
year="2006"
Cross-Language Program Analysis and Refactoring
複数のプログラミング言語を対象としたメタモデルを定義して、メソッドの名前変更のリファクタリングをやりました、という論文。JSP などのように一つのファイル内に異なる言語が混ざっているようなものも対象にしているのが特徴らしい。モデルは、抽象構文木とメタモデルへのマップと関係の生成系からなっている。メタモデルの詳細は別の論文に詳しいらしい。実際に物もできているみたいだけど、売り物なので実装の詳細等はまったく不明。
author="Dennis Strein and Hans Kratz and Welf L{\"o}we",
title="{Cross-Language Program Analysis and Refactoring}",
booktitle="Sixth IEEE International Workshop on Source Code Analysis and Manipulation",
publisher="IEEE Press",
pages="207--216",
year="2006"