研究の基本は人です。個人個人の発想を大事にすること、 学生の目線で一緒に考えること、が研究室運営の基本だと考えています。もちろん、 この方針がうまくいくためには、学生側も自分の考え、 自分のやりたい研究がなにかしっかり考える必要があります。 自分がやりたい研究テーマをどんどん提案してください。
ソフトウェア科学は、ソフトウェアの作り方に関する学問です。 本研究室では、ソフトウェアをがりがりたくさん書く人にも向いていますが、 もっと向いているのは、 自分の書いたソフトウェアがきちんと動くかが「気になる」人です。 どんなに高性能、高機能なソフトウェアも正しくなければ意味がありません。 でも、現実に世の中に流布しているソフトウェアはバグだらけです。 そんなソフトウェアを作り続けているのが馬鹿らしくなった人は、 是非本研究室に来て、 正しさの保証されたソフトウェアをつくる方法を一緒に考えてください。 そこでは、｢プログラムのための論理」が主役になります。
研究は、一人で黙々とやる段階も必要ですが、 異なるバックグラウンドや価値観を持つ人と交流して議論をすることも 非常に大事な要素です。 研究室の中だけで、あるいは、教員に与えられた題材だけで良い研究ができる とは限りません。積極的に外に出て、 自分の力でいろいろなことを発見してください。 このために、（１）学生には、研究室の中にこもらず、 外部の研究会等に参加・発表することを奨励しています。 （２）研究室の構成員として、出身の異なる学生（留学生や筑波大学以外の卒業生など）を 積極的に受け入れています。
｢ソフトウェアの正しさの保証」が大目標です。 そのために、（１）プログラム言語に対する理論を展開して正しく 効率良いプログラムを作るための研究を行い、 また、（２）作成されたソフトウェアをモデル検査や定理証明の 手法により検証する研究を行っています。
モデル検査は高速に処理ができる方法ですが、処理しきれない精密な仕様も存在します。 そのような場合、数学的な定理を証明するような形で、コンピュータ上でソフトウェアの性質を検証するのが 「定理証明』の手法です。 ここでは、様々なプログラム言語や論理体系を統一して記述し、 共通する性質を記述したり推論するための論理体系を構築し、 その上で、自動または手動で定理証明が可能な範囲を見つけだすことを目的として研究を行っています。
課題が与えられるを待っているのではなく、 自主的に新しいテーマを開拓する意気込みをもつ人、 「手を動かす」だけや「頭を動かす」だけでなく、 「手も頭も動かす」人を期待します。
研究室のセミナーは、原則として週１回、半日を費やしてとことん議論します。 それ以外には教員と学生の個別のミーティングを随時行います。
内容は、春学期は、文献(ソフトウェア基礎関係の英文の本）の輪講、秋学期は各自の研究テーマに沿った論文紹介もしくは研究報告です。
なお、セミナー以外の拘束時間は最小限にして、学生の自主性を重んじる方針です。
プログラム言語と論理が基本となります。 これについては、以下の科目を学んでおくと良いでしょう。 ただし、これらの科目の履修が必須というわけではなく、 研究室配属後の輪講では、前提知識を仮定せずに勉強します。 研究にあたって一番大事なことは｢やる気」です。 やる気さえあれば研究室配属後に不足している知識を補うことができます。
また、研究の材料を発掘するためには、情報学全般にわたって好奇心をもって接する態度が望まれます。
まず最初に読むとすると以下のいずれかが良いでしょう。
これまでの在籍者の進路は、 (学類卒業後に大学院に進学した後)、 情報系の企業を中心に、 関連業界に幅広く就職しています。 (NTT、NEC, 大日本印刷、三菱電機、楽天、Yahoo! Japan, カプコン、 ドワンゴ etc.)
学生１人１台のノートPCとワーキングスペース (広い机/椅子)を確保します。
インターネット時代になっても良質の出版物の重要性は残りますから、本をどんどん買いたいと思っています。
ソフトウェアの理論は難しいと言われます． 論理など数学的な道具立てを用いて深い理解を追求するので， とっつきにくい事がその原因でしょう．しかし，苦労なしに人より抜きん出ることはできません． 今，ソフトウェアの世界では、論理がわかる人に対する 需要が高まっています． プログラミングを初めとする情報学の幅広い知識を身につけた皆さんが、次にやるべきことは， １点か２点に絞って「深さ」を追求することです。プログラミングの仕組みを論理的に説明する 理論を知り、それを生かしたソフトウェアを作ることは、皆さんの知的好奇心を大いにくすぐる 格好の題材になると思います。
誰でも書けるプログラムを素早く大量に書く能力より， 正しさを保証しやすいプログラムを書く能力や、プログラムの正しさを理解す る(そして、可能ならば正しさを示す) 能力を身につけてください． 当研究室は，プログラムや論文の「数」や「量」を誇りたい人には向きません． 質の高い仕事を１つ１つ達成したい人向けです．
プログラミングを「がんがん」できることに越したことはありませんが、 むしろ、『よく考えられたプログラム』をしっかり書くことがこの研究室の目標です。 ゆっくりしたペースで着実にものを考えられる人には居心地がよいことでしょう。
研究室見学をしたい人は、教員あてにメイ ル等で見学時間の相談をしてください。
今年の研究室紹介担当は、B4の藤原と矢口です。
担当者のE-mailは haizoku at logic.cs.tsukuba.ac.jp です。(at を@に置き換えてください）。
また、その他の学生からも、各自の観点から率直な意見が聞けると思います。 （本当に自分にふさわしい研究室かどうかは、在籍する学生から直接取材して、 自分自身でしっかり判断してください。）