Hiroshi Unno 研究室

主宰者：Hiroshi Unno
東北大学

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

Unno研究室では、プログラムの正確さを自動で検証する方法の開発に取り組んでいます。具体的には、プログラムが実際に期待どおりに動作するか、あるいは無限ループに陥らないかといった性質を数学的に証明する技術を研究しており、C言語やRust、確率的プログラムなど、様々なプログラミング言語を対象としています。これらの検証問題を制約充足問題や論理式の満足可能性問題へ変換し、効率的なソルバーを用いて自動的に解く手法を採用しています。 研究のもう一つの特徴は、型システムと論理の関連性を活用した検証方法の設計です。研究室では、プログラムの性質を型注釈で表現する「細分化型システム」や、計算の過程で起こる事象の時間的な性質を検証する「時間的エフェクト」など、従来の型システムを拡張した新しい理論的枠組みを開発しています。さらに、線形計画法の双対性の概念をプログラム検証に応用したり、神経回路網を用いた帰納的不変式の発見を試みたりするなど、様々な数学的アプローチを融合させることで、より実用的で表現力の高い検証技術の構築を目指しています。

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

外部リンク

関連研究室(8 件)

研究成果（16 件）

続きを表示（残り 6 件）

科研費（0 件）

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

所属学会・役職（0 件）

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