河辺 義信

「自分の書いたプログラムにバグがないことを，どうすれば保証できるのだろう？」「最近はインターネットで買い物ができて便利だけど，安全性に問題はないのだろうか？安心させてくれるといいのだけれど…」．．．こうした疑問に答えるのが，さまざまなコンピュータシステムの正しさを証明する手法，フォーマルメソッド（形式手法）です．たとえば，インターネット電子投票システムから個人情報漏洩が起きないことを，フォーマルメソッドで証明できます．我々の研究室では，セキュリティプロトコル・ウェブサービス・分散システム・組み込みソフトウェアなどを，正しく・安全に作る技術を研究しています．なかでも，匿名性（個人情報が漏れないこと）の検証理論や，通信プロセス理論に基づくネットワークプログラミング言語の開発，分散システム・アルゴリズムの形式検証に，力を入れています．