Naoki Nishida 研究室

主宰者：Naoki Nishida
名古屋大学

AI 要約（直近 5 年の研究成果）

Naoki Nishida研究室では、プログラムやシステムの動作を数学的に検証・解析する手法の開発に取り組んでいます。特に、条件付きの項書き換え体系という形式的なモデルを用いて、プログラムの振る舞いを厳密に扱うことに注力しています。この体系では、整数やビット列といった実際のデータ型を直接組み込むことができるため、現実的なプログラムの性質をより正確に分析することが可能です。 研究の中心的な課題は、書き換え規則の適用と論理的な等価変換が複雑に絡み合う問題への対処です。この相互作用が解析を困難にし、実装時に膨大な計算量を招いていました。研究室では、存在量化された制約を持つ項に対する最も一般的な書き換え操作の概念を新たに導入することで、この問題の解決を目指しています。また、システムがエラー状態に達しないことを保証する問題を、到達可能性の判定問題として定式化し、その判定可能性の条件を明らかにする研究も進めています。 さらに、並行プログラムの逆向き実行に関する研究にも取り組んでいます。プログラムを前へも後ろへも実行できる可逆性は、非決定的な計算において特定の状態に巻き戻す際に有用です。これまで順序型プログラムの可逆性は深く研究されていましたが、複数の処理が並行して進行する場合の理論と実装はほとんど発展していませんでした。研究室では、通信を伴う並行プログラムの可逆実行技法を形式的に定義し、実装することで、この空白を埋める努力を続けています。

※ AI（Claude）が、公開されている論文要旨から研究の問い・手法・主要な発見を事実情報として抽出・再構成して自動生成しています。誤りを含む可能性があるため、正確性は研究室公式情報でご確認ください。

外部リンク

関連研究室(8 件)

研究成果（10 件）

科研費（0 件）

まだデータがありません（KAKEN 取り込み後に表示）。

所属学会・役職（0 件）

まだデータがありません（学会データ連携後に表示）。