論文へのリンクについて: 論文のアップロードは大会の直前に行われます. 現在リンク切れとなっておりますが, ご容赦下さい.
会場はすべて東京大学 工学部 新2号館にあります. また, 受付は, 工学部新2号館の正面玄関の近くで行います.
| 特別会場 | A会場 | B会場 | C会場 | ポスター会場・懇話会 | |
| 213大講堂 | 221講義室 | 222講義室 | 223講義室 | フォーラム | |
| 9/13(水) 10:00-12:00 |
情報爆発 | コンパイラ | セキュリティ検証 | ||
| 9/13(水) 13:30-15:30 |
Webアプリケーション | プログラミング言語 | 仕様検証システム | ||
| 9/13(水) 16:00-17:30 |
検索 | ラムダ計算 | モデル検査 | ||
| 9/14(木) 10:00-11:30 |
形式的ソフトウェア設計 | XML・HTML | 定理証明系による検証 | ||
| 9/14(木) 13:00-13:30 |
理事長挨拶、表彰式 | ||||
| 9/14(木) 13:30-15:00 |
招待講演(1) | ||||
| 9/14(木) 15:30-17:30 |
ポスター・デモ | ||||
| 9/14(木) 17:00-19:00 |
懇話会＠フォーラム | ||||
| 9/15(金) 10:00-12:00 |
制約・モデル化 | 関数プログラミング・型システム | 様相論理 | ||
| 9/15(金) 13:30-15:00 |
招待講演(2) | ||||
| 9/15(金) 15:30-16:30 |
ユビキタス・分散アプリケーション | 書換えシステム | カテゴリー理論 |
| [1A-1] |
Hybrid cc における区間計算に基づいた離散変化処理方式 ○石井 大輔（早稲田大学大学院理工学研究科）
上田 和紀（早稲田大学理工学術院）
細部 博史（国立情報学研究所） |
| [1A-2] |
ユーザの閲覧履歴に基づくオンライン検索支援システム ○永井 洋一（東京大学新領域創成科学研究科） |
| [1A-3] |
データグリッドのためのポリシーベースの協調モデル ○高橋 直久（名工大）
片山 喜章（名工大）
R. S. Bhuvaneswaran（名工大） |
| [1A-4] |
分散プロセス計算のLMNtalへのエンコーディング ○上田 和紀（早稲田大学） |
| [1B-1] |
双方向CTLによるJava最適化器の生成 ○方 玲（東京工業大学大学院情報理工学研究科）
佐々 政孝（東京工業大学大学院情報理工学研究科） |
| [1B-2] |
中間コードを表すプログラム依存グラフの操作的意味 ○伊藤 宗平（東京工業大学大学院情報理工学研究科）
萩原 茂樹（東京工業大学大学院情報理工学研究科）
米崎 直樹（東京工業大学大学院情報理工学研究科） |
| [1B-3] |
静的単一代入形式上で通常形式部分冗長除去を実現する汎用的手法 ○今橋 孝典（東京工業大学大学院情報理工学研究科）
伊藤 陽（東京工業大学大学院情報理工学研究科）
佐々 政孝（東京工業大学大学院情報理工学研究科） |
| [1B-4] |
目的コードの精査によるCOINSコンパイラ・バックエンドの最適化の改良 ○米倉 翔一(東京工業大学大学院情報理工学研究科)
佐々 政孝(東京工業大学大学院情報理工学研究科) |
| [1C-1] |
モデル検査器を用いたプロトコルのDoS攻撃耐性解析 ○池田 立野（東京工業大学大学院情報理工学研究科）
西崎 真也（東京工業大学大学院情報理工学研究科） |
| [1C-2] |
電子投票プロトコルの匿名性検証のための関数部分知識モデル ○川本 裕輔（東京大学大学院情報理工学系研究科）
真野 健（NTTコミュニケーション科学基礎研究所）
櫻田 英樹（NTTコミュニケーション科学基礎研究所）
萩谷 昌己（東京大学大学院情報理工学系研究科、NTTコミュニケーション科学基礎研究所） |
| [1C-3] |
定理証明を用いたWide Mouth Frog Protocolの検証 ○安田 武史（関西学院大学理工学研究科）
高橋 和子（関西学院大学理工学部） |
| [2A-1] |
回線切断に頑健なWebエージェントMiSpiderについて ○深萱 裕二郎（名古屋工業大学大学院）
大囿 忠親（名古屋工業大学大学院）
新谷 虎松（名古屋工業大学大学院） |
| [2A-2] |
A Web Service Architecture for Bidirectional Updating ○林 康史（東京大学大学院情報理工学系研究科）
劉 東喜（東京大学大学院情報理工学系研究科）
江本 健斗（東京大学大学院情報理工学系研究科）
松田 一孝（東京大学大学院情報理工学系研究科）
胡 振江（東京大学大学院情報理工学系研究科）
武市 正人（東京大学大学院情報理工学系研究科） |
| [2A-3] |
ウェブコンテンツ配信スケジューラのための制約処理系の設計 ○平石 広典（株式会社ウィズダムテック）
溝口 文雄（株式会社ウィズダムテック、東京理科大学） |
| [2A-4] |
Webアプリケーションのためのサービスマイグ レーションの実現とその応用 ○田辺 正喜（名古屋工業大学大学院情報工学専攻）
大囿 忠親（名古屋工業大学大学院情報工学専攻）
伊藤 孝行（名古屋工業大学大学院産業戦略専攻）
新谷 虎松（名古屋工業大学大学院情報工学専攻） |
| [2B-1] |
継続を基本とする言語 CbC による分散プログラミング ○河野 真治（琉球大学工学部）
渕田 良彦（琉球大学工学部）
宮國 渡（琉球大学工学部） |
| [2B-2] |
マルチスレッド環境における実時間ごみ集めのためのスレッド再開バリア ○鵜川 始陽（京都大学大学院情報学研究科）
花井 亮（京都大学大学院情報学研究科）
八杉 昌宏（京都大学大学院情報学研究科）
湯淺 太一（京都大学大学院情報学研究科） |
| [2B-3] |
AOP言語への織り込みインターフェイスの導入 ○境 顕宏（九州工業大学）
鵜林 尚靖（九州工業大学）
玉井 哲雄（東京大学） |
| [2B-4] |
アスペクト指向プログラミングにおけるテストに基づいたポイントカットの提案 ○櫻井 孝平（東京大学大学院総合文化研究科）
増原 英彦（東京大学大学院総合文化研究科） |
| [2C-1] |
仕様の自動検証に適したLTLフラグメント ― 実現集合を表す決定性オートマトン構成の立場から― ○島川 昌也（東京工業大学 大学院情報理工学研究科）
萩原 茂樹（東京工業大学 大学院情報理工学研究科）
米崎 直樹（東京工業大学 大学院情報理工学研究科） |
| [2C-2] |
タブロー法を用いたContinuation based Cプログラムの検証 ○下地 篤樹（琉球大学）
河野 真治（琉球大学） |
| [2C-3] |
グリッド計算機を利用した並列仕様検証に関する研究 ○大滝 大輔（東京工業大学大学院情報理工学研究科）
安藤 崇央（東京工業大学大学院情報理工学研究科）
米崎 直樹（東京工業大学大学院情報理工学研究科） |
| [3A-1] |
ニュースディレクトリの構築と検索のための方式 ○劉 斌（リュウ ヒン）（東京工業大学大学院情報理工学研究科）
ファム ヴァンハイ（東京工業大学大学院情報理工学研究科）
ジェグ ケン（東京工業大学大学院情報理工学研究科）
徳田 雄洋（東京工業大学大学院情報理工学研究科） |
| [3A-2] |
blog検索エンジンもぶろげっとへの動画検索機能の導入 ○高地 利幸（電気通信大学）
林 貴宏（電気通信大学）
尾内 理紀夫（電気通信大学） |
| [3A-3] |
Suffix Array を利用した正規表現検索 ○吉川 拓哉（東京大学学際情報学府学際情報学専攻）
田中 久美子（東京大学情報理工学系研究科） |
| [3B-1] |
Completeness of Modal Proofs for First-Order Predicate Proofs ○安部 達也（東京大学） |
| [3B-2] |
λμ計算の抽象機械 ○藤田 憲悦（群馬大学工学部） |
| [3B-3] |
代入定理と永続強正規化可能性 ○龍田 真（国立情報学研究所）
Mariangiola Dezani-Ciancaglini（Torino Univ） |
| [3C-1] |
Model-checking of a Multi-threaded Operating System ○Nicolas Marti（東京大学）
Reynald Affeldt（産総研 RCIS）
Akinori Yonezawa（東京大学, 産総研 RCIS） |
| [3C-2] |
モデル検査を用いたNAT越え通信ソフトウエア検証の研究 ○西山 裕之（東京理科大学理工学部）
溝口 文雄（東京理科大学理工学部） |
| [3C-3] |
遷移関係の詳細化による正則モデル検査の再構成と拡張 ○櫻田 英樹（NTTコミュニケーション科学基礎研究所）
萩谷 昌己（東京大学、NTTコミュニケーション科学基礎研究所） |
| [4A-1] |
Toward a Domain Description with CafeOBJ ○有本 泰仁（北陸先端科学技術大学院大学情報科学研究科）
中村 正樹（北陸先端科学技術大学院大学情報科学研究科）
二木厚吉（北陸先端科学技術大学院大学情報科学研究科） |
| [4A-2] |
ポリシ管理システムのための検査手法 ○前田 直人（NECインターネットシステム研究所）
猪鹿倉 知広（NECインターネットシステム研究所）
登内 敏夫（NECインターネットシステム研究所） |
| [4A-3] |
サービス合成におけるセキュリティポリシーの抽象化による整合性の検証 ○小野 康一（日本アイ・ビー・エム株式会社 東京基礎研究所）
中村 祐一（日本アイ・ビー・エム株式会社 東京基礎研究所）
佐藤 史子（日本アイ・ビー・エム株式会社 東京基礎研究所）
立石 孝彰（日本アイ・ビー・エム株式会社 東京基礎研究所） |
| [4B-1] |
Web部分情報抽出システムとその応用 ○韓 浩(カン コウ)（東京工業大学大学院情報理工学研究科）
徳田 雄洋（東京工業大学大学院情報理工学研究科） |
| [4B-2] |
アクセス制御機能を持つ利用者適応型XML文書処理系 ○串松 陽介（山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻）
渡辺 喜道（山梨大学大学院医学工学総合研究部） |
| [4B-3] |
双方向変換に基づくウェブページ更新機構 ○中野 圭介（東京大学大学院情報理工学系研究科）
森畑 明昌（東京大学大学院情報理工学系研究科）
胡 振江（東京大学大学院情報理工学系研究科）
武市 正人（東京大学大学院情報理工学系研究科） |
| [4C-1] |
Formal Verification of Arithmetic Functions in SmartMIPS Assembly ○Reynald Affeldt（産総研 RCIS）
Nicolas Marti（東京大学） |
| [4C-2] |
代数付きπ計算によるデータベースの記述と検証 ○宮本 賢治（産業技術総合研究所システム検証研究センター、京都大学大学院情報学研究科）
清野 貴博（産業技術総合研究所システム検証研究センター）
竹内 泉（産業技術総合研究所システム検証研究センター） |
| [4C-3] |
自動証明系と定理証明支援系の連携によるポインタ操作プログラムの検証について ○湯浅 能史（産業技術総合研究所システム検証研究センター）
武山 誠（産業技術総合研究所システム検証研究センター）
関澤 俊弦（産業技術総合研究所システム検証研究センター、大阪大学大学院情報科学研究科）
田辺 良則（産業技術総合研究所システム検証研究センター、東京大学大学院情報理工学系研究科）
高橋 孝一（産業技術総合研究所システム検証研究センター） |
| [IT-1] |
プログラミング言語SML＃の開発とその基礎理論 ―多相型言語の基礎研究はもはや時代遅れか?― 大堀 淳（東北大学電気通信研究所） |
| [P-1] |
DRMシステムの相互運用性評価に関する研究 近藤順也（北陸先端科学技術大学院大学情報科学研究科） |
| [P-2] |
双方向変換に基づくウェブページ更新機構 中野圭介、森畑明昌、胡振江、武市正人（東京大学大学院情報理工学系研究科） |
| [P-3] |
A Web Service Architecture for Bidirectional Updating 林康史、劉東喜、江本健斗、松田一孝、胡振江、武市正人（東京大学大学院情報理工学系研究科） |
| [P-4] |
関数プログラムの系統的探索 片山 晋（宮崎大学工学部） |
| [P-5] |
双方向CTLによるJavaプログラム最適化器の生成 方玲、佐々政孝（東京工業大学大学院情報理工学研究科） |
| [P-6] |
汎用連想計算エンジンGETA 西岡真吾、小池勇治、高野明彦（国立情報学研究所） |
| [P-7] |
連想検索を用いた分散型検索インタフェース 小池勇治、西岡真吾、高野明彦（国立情報学研究所） |
| [P-8] |
Haskellのためのπ計算に基づくネットワークプログラミングフレームワーク 今井敬吾、結縁祥治、阿草清滋（名古屋大学情報科学研究科） |
| [P-9] |
対話型定理証明支援系 Agda の紹介 岡本圭史、湯浅能史（産業技術総合研究所システム検証研究センター） |
| [P-10] |
「ソフトウェア論文」について 上田和紀（日本ソフトウェア科学会 編集委員長） |
| [5A-1] |
E-Origami System Eos ○Asem Kasem（筑波大学）
Tetsuo Ida（筑波大学）
Hidekazu Takahashi（筑波大学）
Mircea Marin（筑波大学）
Fadoua Ghourabi（筑波大学） |
| [5A-2] |
Logical and Algebraic Formulation of Origami Axioms ○Fadoua Ghourabi（筑波大学）
Tetsuo Ida（筑波大学）
Hidekazu Takahashi（筑波大学）
Mircea Marin（筑波大学）
Asem Kasem（筑波大学） |
| [5A-3] |
筋肉バネモデルに基づく生体シミュレータの設計 ○松田 啓二（東京理科大学理工学研究科経営工学専攻）
平石 広典（株式会社ウィズダムテック）
溝口 文雄（東京理科大学理工学部経営工学科） |
| [5B-1] |
Representing Cyclic Structures as Nested Datatypes ○浜名 誠（群馬大学）
Neil Ghani（Nottingham University）
Tarmo Uustalu（Tallinn University of Technology）
Varmo Vene（University of Tartu） |
| [5B-2] |
弱逆関数の自動導出によるプログラムの並列化 ○森田 和孝（東京大学大学院情報理工学系研究科）
森畑 明昌（東京大学大学院情報理工学系研究科）
胡 振江（東京大学大学院情報理工学系研究科）
武市 正人（東京大学大学院情報理工学系研究科） |
| [5B-3] |
多相型レコードに基づくRubyオブジェクトの型推論に関する考察 ○松本 宗太郎（筑波大学 システム情報工学研究科）
南出 靖彦（筑波大学 システム情報工学研究科） |
| [5B-4] |
階層化コントロールオペレータに対する型システムの構築 ○鈴木 輝信（筑波大学システム情報工学研究科）
亀山 幸義（筑波大学システム情報工学研究科） |
| [5C-1] |
A Logic for Finite Resources ○上出 哲広（産業技術総合研究所システム検証研究センター） |
| [5C-2] |
函数記号付一階様相μ計算 ○岡本 圭史（産業技術総合研究所システム検証研究センター）
木下 佳樹（産業技術総合研究所システム検証研究センター） |
| [5C-3] |
階層的グラフ構造の記述と検証のための様相論理 ○田辺 良則（産業技術総合研究所システム検証研究センター、東京大学大学院情報理工学系研究科）
萩谷 昌己（東京大学大学院情報理工学系研究科、NTTコミュニケーション科学基礎研究所） |
| [IT-2] |
再帰プログラムの幾何（Geometry of Recursive Programs） 長谷川 真人（京都大学数理解析研究所） |
| [6A-1] |
携帯電話アプリケーションによるモバイルなセンサネットワーク構築支援システム ○大林 真人（東京都立産業技術研究センター）
西山 裕之（東京理科大学）
溝口 文雄（東京理科大学） |
| [6A-2] |
Look and X : コラボレーション支援における統合インタフェースの設計と実装 ○畑 寛之（東京理科大学大学院理工学研究科）
平石 広典（株式会社ウィズダムテック）
西山 裕之（東京理科大学理工学部）
溝口 文雄（東京理科大学理工学部） |
| [6B-1] |
条件付き項書換えを定義する線形な項書換え系 ○服部 哲（北陸先端科学技術大学院大学情報科学研究科） |
| [6B-2] |
左線形項書換えシステムの合流性 ○岩見 宗弘（島根大学） |
| [6C-1] |
Generic Forward and Backward Simulations ◯蓮尾 一郎（University of Nijmegen）
Bart Jacobs（University of Nijmegen）
Ana Sokolova（Radboud Univ） |
| [6C-2] |
Weighted Kripke Structures and Refinement of Models 亀山 幸義（筑波大学）
木下 佳樹（産業技術総合研究所システム検証研究センター）
○西澤 弘毅（産業技術総合研究所システム検証研究センター） |