---------------------------------------------------------------
産業技術総合研究所算譜科学グループ研究速報
(AIST Programming Science Group Technical Report)[AIST-PS-2004-002]
シンポジウム「システム検証の科学技術」予稿集: 平成16年2月4-6日
於: 大阪梅田スカイビル
2004年2月
全編[pdf 11.5MB]

---------------------------------------------------------------
表  紙 [38KB]
はじめに[18KB]
  システム検証研究ラボ長 木下佳樹
目  次
<基調講演>
◇システム検証技術に期待するもの [55KB]
  田中英彦(東京大学大学院情報理工学系研究科)
<招待講演>
◇ より品質の良いソフトウェアの作成のために [56KB]
  大蒔和仁(産業技術総合研究所情報処理研究部門および研究コーディネータ)
<チュートリアル>
◇ モデル検査入門 [1207KB]
  高橋孝一(産業技術総合研究所)
◇ 型理論での定理証明 [107KB]
  武山誠(産業技術総合研究所)
◇ システムモデル化と形式仕様記述 [56KB]
  荒木啓二郎(九州大学)
<招待講演>
◇ 判断と導出の理論 [56KB]
  佐藤雅彦(京都大学大学院情報学研究科)
<一般講演>
◇ A Type System for Optimization Verifying Compilers [1248KB]
  松野裕,佐藤周行(東京大学)
◇ 書換系と抽象解釈を用いた検証技法 [722KB]
  高井利憲(科学技術振興機構(CREST))
◇ Aliasing-PDS: オブジェクト指向プログラムのモデル検査のための新しい計算モデル [1148KB]
  新田直也(奈良先端科学技術大学院大学)
◇ 抽象解釈にみられる圏論的構成について [947KB]
  西澤弘毅(産業技術総合研究所)
◇ 値渡しゲームの圏における深さ優先戦略について[80KB]
  松岡聡(産業技術総合研究所)
◇ 機能競合の検出を目的とした限定モデル検査手法の改良 [482KB]
  横川智教,土屋達弘(大阪大学),中村匡秀(奈良先端科学技術大学院大学),
  菊野亨(大阪大学)
◇ 時相論理式を用いた抽象化法のツール化に向けて [345KB]
  田辺良則(科学技術振興機構(CREST)),高橋孝一(産業技術総合研究所),
  高井利憲(科学技術振興機構(CREST))
◇ Towards Real-Environment Model Checking [56KB]
  萩谷昌己,佐藤治(東京大学),Richard Potter(東京大学および科学技術
  振興機構(PRESTO)),山本光晴(千葉大学)
◇ セキュリティ・プロトコル仕様の論理的翻訳 [144KB]
  櫻田英樹(日本電信電話株式会社NTTコミュニケーション科学基礎研究所)
◇ Kripke構造の模倣性に関する基本的性質および縮小化・抽象化に対する証明支援系による
  形式化 [834KB]

  高木理,武山誠,渡邊宏(産業技術総合研究所)
<招待講演>
◇ ソフトウェアエンジニアリングセンターについて [55KB]
  祝谷和宏(経済産業省商務情報政策局情報処理振興課)
<一般講演>
◇ ケーススタディ: モデル検査と定理証明を用いた鉄道信号制御システムの検証[1202KB]
  亀山幸義(筑波大学および科学技術振興機構),中島一(筑波大学)
◇ モデル検査による組み込みソフトウェア仕様書の検証実験 [55KB]
  水口大知, 早水公二, 渡邊宏(産業技術総合研究所),篠崎孝一(関西電力株式
  会社),石井健志, 吉田雅昭(東光精機株式会社), 眞鍋慎一, 横山幸生, 栃谷陽一
  (メルコ・パワー・システムズ株式会社)
◇ 大規模事務処理システムにおける形式手法の適用 [546KB]
  佐原伸(日本フィッツ株式会社)
◇ 組込みシステムの開発工程への形式的手法導入にむけた取り組み [67KB]
  大崎人士(産業技術総合研究所)
◇ 法定計量器の組込ソフトウェアの照合技術について [56KB]
  松岡聡,田中充,木下佳樹,高橋孝一,浜川剛,伊藤武(産業技術総合研究所)
<招待講演>
◇ 探索理論による合理的なテストと検証指向設計 [55KB]
松尾谷徹(デバッグ工学研究所および東京理科大学)
<一般講演>
◇ 3層Webアプリケーションにおける整合性検査のためのデータ辞書 [798KB]
  尾崎哲平(名古屋大学)
◇ 形式仕様記述言語VDM++による形式モデルの構築と 関数型言語Erlangによる実行
  [56KB]  

  時松誠治,日下部茂,荒木啓二郎(九州大学)
◇ 安全性を保証するアクティブソフトウェアの構成法 [1147KB]
  渡邉勝正,井上晶広,真嶋利彰,伴野 充,中西正樹,山下 茂(奈良先端科学技術
  大学院大学)
◇ プロトコルにおける記憶領域のコスト解析のための型付きπ計算 [60KB]
  西崎真也,池田立野(東京工業大学)
◇ 単項二階論理とオートマトン・様相μ計算 [151KB]
  池上大介(科学技術振興機構(CREST))

奥付[24KB]