Koji Nakazawa 研究室

主宰者：Koji Nakazawa
名古屋大学

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

本研究室は、プログラムが正しく動作することを数学的に保証する「プログラム検証」に関する研究を展開しています。特に、メモリ領域の操作を含むプログラムの正当性を証明する方法論の開発に取り組んでいます。具体的には、メモリ構造の操作に対応した論理体系（分離論理や関連する拡張論理）の構築と、これらの論理における推論規則の性質を数学的に解析することが中心課題です。 プログラムの正当性を自動的に検証するために、本研究室では「循環証明系」という特殊な証明体系を用いた手法を研究しています。この体系は帰納的な性質を扱うのに適していますが、一般的な証明体系の望ましい性質である「カット除去性」が必ずしも成り立たないという課題があります。研究室では、複数の論理体系に対してカット除去性が失敗することを証明し、その構造を解明しています。 さらに、配列やポインタ演算に対応した拡張の相対的完全性を示すなど、実務的なプログラム検証に対応できる論理体系の開発も進めています。これらの研究を通じて、より実用的で信頼性の高いプログラム検証基盤の構築を目指しています。

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

外部リンク

関連研究室(8 件)

研究成果（9 件）

科研費（0 件）

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

所属学会・役職（0 件）

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