タスクがいろいろ積み上がってるけどどうにもやる気にならないので現実逃避的にドライブへ。国道 24 号を南下して、葛城、太子、河南、和泉あたりの道の駅に寄りながら関空の対岸まで。帰りは泉南から高速道路。第二京阪道と近畿道が門真で接続したおかげで楽になってる。最近はドライブしても知ってる道だと結局考え事してリフレッシュになってなかったけど、今日は奈良から先は知らないところだったからリフレッシュできたかな。

コメント追加

投稿者 kw : 2010/05/29 23:44:00 JST #

読了。

コメント追加

投稿者 kw : 2010/05/16 13:12:00 JST #

Java プログラムに対し、新しい型と型間の半順序関係を定義してプログラム中に型を記述すれば後は型推論してくれるシステムの話。型付け規則は given なので、検査したいことをうまく書くことができれば型と関係の定義だけですむので楽。論文では例として、JNI プログラムにおいて Java と C で受け渡される整数を変な使い方をしないか検査するというのと、Javari ベースな不変性解析が挙げられている。もしかすると情報流解析の型システムもこの仕組みに載せられるかも。

author="David Greenfieldboyce and Jeffrey S. Foster",
title="{Type Qualifier Inference for Java}",
booktitle="OOPSLA '07",
publisher="ACM",
pages="321--336",
year="2007"

http://doi.acm.org/10.1145/1297105.1297051

コメント追加

投稿者 kw : 2010/05/14 17:08:00 JST #

読了。

コメント追加

投稿者 kw : 2010/05/13 21:44:00 JST #

昨日のドライブまとめ。もとの予定ではもっと西のほうに行くつもりだったけど、宝塚あたりの渋滞が嫌で紀伊半島を反時計回りにぐるっと回ることに。阪和道の南端まで行って、海沿いの 42 号を走って、紀勢道で帰るルート。行きの下津辺りと帰りの亀山辺りの渋滞で 2,3 時間ロスした感じで、結局渋滞は避けられず。いつも通りちょくちょく道の駅に寄りながら移動。すさみの辺りでオート三輪とすれ違ってびっくりした。子供の頃に 1,2 回見たことがあるくらいで、今でも走ってるとは思わなかった。昨日の走行距離は 580km 程度。渋滞で左足がしんどかった。もとの予定だったところは休日 1000 円のうちに行くつもり。

コメント追加

投稿者 kw : 2010/05/04 11:26:00 JST #

並行プログラムを対象とする情報流解析の型システムが非干渉性に対して健全であることを Isabelle/HOL を使って示したという論文。逐次プログラムの非干渉性は、高機密度のデータのみが異なる初期状態から実行した結果が区別できないことだけど、並行プログラムの場合は利アクティブ性を考慮して bisimilarity を要求する。それと、スケジューリングの方法によって実行が変わるのでスケジューラを考慮できるようにする。というセッティングのもとで健全性を証明。

author="Gilles Barthe and Leonor Prensa Nieto",
title="{Formally Verifying Information Flow Type Systems for Cuncurrent and Thread Systems}",
booktitle="FMSE '04",
publisher="ACM",
pages="13--22",
year="2004"

http://doi.acm.org/10.1145/1029133.1029136

コメント追加

投稿者 kw : 2010/05/02 13:49:00 JST #

読了。

コメント追加

投稿者 kw : 2010/05/01 18:28:00 JST #