情報処理学会東海支部 主催講演会

開催日：

2002年10月16日（水）15:00-16:30

会場：

名古屋大学工学部9号館330号室（交通は：http://www.nagoya-u.ac.jp/sogo/higashiyama.html 参照．35番の建物の3階）

主催：

情報処理学会東海支部

協賛：

IEEE Nagoya Section

参加費：

無料（参加資格は問いません）．また事前申し込み不要．会場へ直接おこしください．

概要：

ネットワークを介して協調動作するプログラムを形式的に記述する体系として，プロセス代数がある．我々は，π計算と呼ばれるモバイルプロセス代数に基づくプログラミング言語 Nepi を設計，実装している．Nepi を用いることによって，プロトコルなどを簡潔かつ厳密に記述することができ，その記述は形式的な検証に適する．Nepi システムは，同期通信を実現するためにある種の2層コミットを実装している．我々はこの実装を Lynch の I/O オートマトンによって形式化し，Larch 定理証明器を用いて正しさを形式的に証明した．講演では，Nepi システムの概要と，その実装の正しさの証明について解説する．

講演題目・講師：

「モバイルプロセス代数に基づくプログラミング言語 Nepi と，その実装の正しさの検証」

真 野 　健 氏 （日本電信電話株式会社 NTTコミュニケーション科学基礎研究所

社会情報研究部　分散協調理論研究グループ　主任研究員 ）　

問い合わせ先：

　結縁 祥治（名古屋大学大学院工学研究科情報工学専攻学）
　〒464-8603　名古屋市千種区不老町
　Tel: 052-789-3649　Fax: 052-789-3810
　E-mail： yuen＠nuie.nagoya-u.ac.jp
　http://www.agusa.nuie.nagoya-u.ac.jp/person/yuen/

又は
　社団法人 情報処理学会東海支部 事務局
　〒460-0003　名古屋市中区錦2-17-21�鰍mＴＴデータ 東海支社内
　TEL:（052）204-4517 FAX：（052）204-4521　　　
　E-mail: t-ipsj＠tcp-ip.or.jp
　http://www.ipsj.or.jp/sibu/tokai/