情報玉手箱

  • ホーム
  • 特集
    • サイエンス・ウィズ・情報
    • 弱きを助ける情報学
    • 情報システム学とセキュリティ
    • 情報学の研究者たちの喜怒哀楽
    • 最適化技術の応用・実践
    • 見えない現象を見える化する
    • 身体の情報処理がこころをつくる
    • 情報学と名大スパコン不老
    • 情報学と自然言語処理
    • 新型コロナと情報
  • 情報玉手箱とは
  • Menu

  • Sidebar

  • Prev

  • Next

  • Search

  1. ホーム>
  2. 情報システム学専攻

教員紹介:西田 直樹(にしだ なおき)

研究内容

バグのない高信頼なソフトウェアを作成することは現代社会において非常に重要です。通常はプログラムが正しいことを検証することで高信頼なプログラムを開発します。私の研究では、関数型言語だけでなく命令型言語の計算モデルとも言える制約付き項書換え系を用いて、C言語プログラムが仕様に相当する関数と等価であることを自動証明する研究に取り組んでいます。自動証明には書換え帰納法と呼ばれる人間が行う証明に沿った証明原理を利用しています。この証明法の自動化では、人間がどのように証明を完成させるかという知識を計算モデルの上で形式化します。また、書換え帰納法による検証技術を大学のプログラミング演習で提出されるプログラムが正しいことの検証だけでなく、車載組込み制御システムの検証への応用にも取り組んでいます。その他、与えられたプログラムが定義する関数の逆関数を定義するプログラムを自動生成するプログラム逆化や、可逆計算モデルの研究にも取り組んでいます。

所属・連絡先など

  • 情報システム学専攻/コンピュータ科学科情報システム系
  • E-mail: nishida@i.nagoya-u-ac-jp
  • 居室:IB電子情報館南棟5階589
  • 個人HP:https://www.trs.css.i.nagoya-u.ac.jp/~nishida/index-jp.html

2020年12月8日情報システム学専攻項書換え系, 計算モデル, プログラム検証, プログラム逆化, 可逆計算, 教員紹介, 情報システム学専攻, コンピュータ科学科, 情報システム系

Posted by Naoki Nishida

教員紹介:青木 摂之(あおき せつゆき)
Next
教員紹介 森崎 修司 (もりさき しゅうじ)
Prev

関連記事

No Image

教員紹介:倉地 亮(くらち りょう)

研究内容 近年,組込みシステムのソフトウェアは大規模になり,複雑化が著しいです. ...

No Image

教員紹介:楫 勇一(かじ ゆういち)

研究内容 今日の情報化社会では、全てを内包する一つの大 き な ネ ット ワ ー ...

No Image

教員紹介:永井 亨(ながい とおる)

研究内容 任意の異方性と分散性のある不均質媒質中の波動場を計算することは地震予知 ...

No Image

IEEE VTS Tokyo/Japan Chapterで2021 Young Researcher’s Encouragement Awardを受賞しました。(情報システム学専攻 安食拓海 M2)

No Image

教員紹介:酒井 正彦(さかい まさひこ)

研究内容 「虫のいないプログラムはない」といわれるほど、誤りのないプログラムを作 ...

タグ

アルゴリズム イベント案内・報告 グローバルメディア研究センター ゲノム コンピュータ科学科 プログラム検証 プログラム逆化 メタヒューリスティクス 人間・社会情報学科 仮想生物 価値創造研究センター 可逆計算 学会発表 心理・認知科学専攻 心理・認知科学系 情報システム学専攻 情報システム系 教員紹介 数理情報学専攻 数理情報系 海外派遣助成 海外渡航 生物リズム 知能システム学専攻 知能システム系 研究グループ紹介 社会情報学専攻 社会情報系 組合せ最適化 組込みシステム研究センター 自然情報学科 著作物紹介 複雑システム系 複雑系科学 複雑系科学専攻 複雑系計算論 複雑系計算論講座 触覚のVR 触覚センサ 触覚ロボット 計算モデル 認知科学 進化 項書換え系 鳥の歌

Copyright © 2023 情報玉手箱 All Rights Reserved.

WordPress Luxeritas Theme is provided by "Thought is free".

PAGE TOP