工学部研究紹介2016｜信州大学

50/80

情報⼯学科⿑藤研究室研究から広がる未来卒業後の未来像生活・自然環境情報センシングシステム・LIFSライダー：空中スギ花粉、粉塵、諏訪湖水質、植物生育の遠隔情報センシングに使用中；工学部キャンパス（上）、長野県諏訪湖（下）での実験の様子安全で安心な生活が保障されるには、どのような情報が必要でしょうか？私達は、身近な生活に係る自然環境を注意深く見つめ、その情報をきちんと理解する技術－センシング技術－の開発を行っています。空気・水・植物等、私達の生活周辺環境が“今”どうなっているのかを、正しく理解することが、安全・安心を確保する第一歩です。それを実現するキーワードが“光”“画像”“IT”です。レーザーや特殊カメラといった、最新の光・画像機器を駆使した、オリジナルな光情報センシングシステムを開発しています。信州の身近な環境から世界観に富むグローバルな環境までを相手にして、安全・安心な生活のための情報発信を目指します。地球と人間は“光”の恵みを上手に使いながら、現在の豊かな自然・生活環境を作りあげてきました。将来の、青空と緑に囲まれた空間に光が満ちあふれている健全な生活環境を想像して下さい。工学技術としての“光”だけではなく、理学・農学・生物学・人間・生活・環境・地球そして宇宙をつなぐ技術として、“光”が活躍する場面は無数にあります。目指すべきは、“光”の新たな可能性への挑戦！発想を実験という体験（やってみることが重要）を通して実現すること、その事実をきちんと理解できる能力を身につけること、をモットーに指導しています。どのような職業についても“へこたれない力”を授けますよ。齊藤保典教授1980年信州大学工学部助手。2004年より現職。学生時代にレーザー光の美しさに魅了され、それが仕事になってしまった。以来、一貫して光センシング技術の開発に従事。光を通じて人間と自然の関係を見続けている。安全・安⼼をサポートする⽣活環境情報の光情報センシング技術製品設計や仕様書の正しさをチェックする（ものづくりへの応用）証明問題のインタラククティブ教材（教育への応用）(数学以外への形式化数学の応用例) 情報⼯学科師⽟研究室研究から広がる未来卒業後の未来像形式化数学記述言語によって、現行数学の全ての定理とその証明をライブラリ化するという壮大な目標をもった国際共同研究プロジェクトに参加しながら、形式化数学と計算機ソフトウエア開発の融合を目指しています。人手による解析や、全ての場合を尽くせるとは限らないテストデータによる試行に頼ることなく、その動作の正しさが数学的に裏付けされたプログラムを開発できる手法の構築を目指しています。学生たちには、論理的思考能力、数理的思考能力を身に付けた情報工学技術者となるように指導しています。師玉康成教授工学博士(慶応義塾大学）1987年防衛大学校理工学研究科研究員、1990年信州大学助手、助教授を経て1995年より同大学教授形式化数学記述言語とそれを用いた計算機検証の研究に従事。主に•数学基礎一般の形式化と検証･ライブラリ編纂•アルゴリズムの動作検証•形式化数学記述言語を用いた論理思考訓練教材の構築に取り組む。師玉研究室では数学定理と証明を計算機のプログラムのような形式化言語で書いてその論理的･数学的正しさを計算機で検査する研究をしています。この検査で正しいことが確かめられた定理と証明を辞書のようにライブラリにする国際共同研究プロジェクトに海外の研究者達とともに参加しています。例えばインターネットのデータ通信に使われる暗号は高度な代数学を用います。現代の科学･工学技術は数学なしには成り立ちません。株式の売買その他、経済活動も高度な数学を利用したコンピュータシステムが主役になっています。数学の研究成果の正しさを、誤りを犯しやすい人手によらず、計算機によって、厳密に、瞬時に検査できる手段は大変重要です。その使い道は定理の正しさを検査するだけではなく、将棋やチェスのルールのように複数の規則に従って、様々な要素や手続き、機能を論理的に組み合わせて作られる工学的なシステムの開発やその動作の検査にも応用できます。例えば計算機のプログラムは入力データから出力データを作る論理的な手続きを形式的な言語で表現したものであり、その動作は数学的な命題として表すことができます。これにより、今までのように、多くのテストデータを入力して処理結果を検査したり、誤りを犯しやすい人手によって動作を一行一行解析したりといった、不完全な方法ではなく計算機によって数学的に厳密に検査することができるようになります。それが正しいと確認されれば、その形式的な記述をそのまま、計算機プログラムに変換して使えば、その動作の正しさが数学的に裏付けされたプログラムを作ることができます。形式化数学記述⾔語と計算機検証48

※このページを正しく表示するにはFlashPlayer10.2以上が必要です