学生の柿下シナイさん（博士前期課程2年、次世代デジタル社会基盤研究領域、青木研究室）が、The 27th International Symposium on Formal Methods (FM 2026) に併催されたDoctoral Symposiumにおいて、Best Presentation Awardを受賞しました。

　FM 2026 Doctoral Symposiumは、FM 2026に併催された博士課程学生を対象としたシンポジウムであり、令和8年5月19日に東京で開催されました。形式手法に関する研究に取り組む博士課程学生が、自身の研究内容や進捗を発表するとともに、他の参加学生や経験豊富な研究者との交流を通じてフィードバックや助言を得ることを目的としています。
　Best Presentation Awardは、同シンポジウムにおいて特に優れた発表を行った学生に授与される賞です。

※参考：FM 2026

■受賞年月日
　令和8年5月19日

■研究題目、論文タイトル等
Towards verified memory allocator for Rust

■研究者、著者
　柿下シナイ

■受賞対象となった研究の内容
　メモリアロケータは、主記憶領域を自動的に管理することで、柔軟なプログラム記述と計算資源の効率的な利用を実現する基盤技術であり、基本ソフトウェアであるオペレーティングシステムをはじめとする様々なシステムで利用されている。本研究では、特に自動運転車のような安全性が重視される用途向けオペレーティングシステムで利用されるメモリアロケータに着目する。その正当性を検証し、メモリアロケータを基盤とするシステム全体の信頼性向上に貢献することを目的とする。本研究では、プログラム検証に基づいた手法を用いる。プログラム検証とは、プログラムの仕様を形式的に記述し、実装がそれを満たすことを論理的に証明する技術である。この手法では、機能要求の充足や欠陥の不在が数学的に証明できるため、欠陥が人命に関わる結果をもたらす自動運転システムなどに適している。本研究の特徴は、システムソフトウェア特有の詳細な実装レベルの性質を効率的に検証するとともに、既存実装に忠実な検証を行う点にある。これにより、すでに利用されている実装を変更することなく、実用されているシステムに後から正しさの保証を与えることができる。

■受賞にあたって一言
　このような賞を頂き、大変光栄に存じます。本研究を支えてくださった研究室の皆様、共同研究先の皆様に感謝申し上げます。

令和8年7月2日