神林研究室 ゼミY について

 

こんにちわ。神林研では、ゼミYについて、次のような方向で進めたいと考えています。ソフトウェア一般について興味のある学生の履修を希望します。

 

次の2つのことを並行して進めます。その2のために、場合によっては、週一以上集まってもらうかもしれません。卒業研究のテーマを早めに決めて、4年生になって慌てないためです。(4年生の前半は就職活動でとても忙しいことがわかりました。)

その1:次の本を輪講形式で読みます。プログラム検証について、日本語で読める数少ない良書です。

        林 晋著 「プログラム検証論」 共立出版

その2:各自の興味ある分野の論文を調査して、内容を理解し要約する練習をする。

            論文は、プログラミング言語やプログラミングシステム、あるいはソフトウェア工学に関するものであればなんでもよい。

            4年生になった時の卒論のテーマを探すことを目的とします。

現在進行中のプロジェクトについては、http://leo.nit.ac.jp/~yasushi/研究室紹介のスライドはこちらを参照してください。

プログラム検証、あるいは広くプログラミング理論とは?

一般に、あるプログラムが正しく動作するかどうかは実行してみないことにはわからない。とはいうものの、むやみに実行して暴走してしまっては困るソフトウェアは多い。(単純な例では、原子炉の制御プログラムを考えればよい。)

そこで、可能な限りプログラムを実行せずに、プログラムの字面だけを見て、その動作を理解できる方法が欲しい。そのような研究が、一般にプログラミング理論と呼ばれる分野であり、最近のソフトウェア工学研究のひとつの主流となっている。

まだ若い分野であり、実用には達していないが、多くの可能性と、「もし実現できたらすごい」という夢のある分野でもある。

そして、おそらく今勉強しておかないと、就職してからはなかなか手のでない分野でもあろうと思います。

というわけで、よいプログラムを書いて、それを生業としよういう心意気の人々を募集します。

また、海外留学を考えている人には、別途個別に相談に乗ります。