寺内研究室

About研究室について

バグのないソフトウェアを目指す。

寺内研究室は、プログラミング言語分野を研究しています。
プログラムが仕様通りに動くかを自動で確かめる「プログラム検証」と、仕様から正しいプログラムを自動でつくる「プログラム合成」を中心に研究しています。
これらの技術を、情報漏洩やタイミング攻撃といったセキュリティの問題に応用する研究も行っています。
型システムや数理論理学、形式言語理論など、これらを支える基礎理論の研究にも取り組んでいます。

Research研究テーマ

寺内研究室では、コンピュータアルゴリズムを使って、プログラムの正しさを機械的に検証したり、正しいプログラムを機械的に合成したりすることで、ソフトウェアの信頼性を高める研究をしています。型システムや数理論理学など、理論に根ざした手法を重視しています。

※イメージ画像

プログラム検証↗

プログラムのコードを解析し、仕様通りに動作するかを検証する研究です。高階関数などを含む高レベルな言語のプログラムを、効率よく検証する技術に取り組んでいます。

※イメージ画像

プログラム合成↗

仕様や入出力の例から、正しいプログラムを自動的につくり出す研究です。サイドチャネル攻撃に強いコードや、安全な正規表現を自動で合成する手法などを研究しています。

※イメージ画像

セキュリティへの応用↗

プログラム検証・合成の技術を、機密情報の漏洩やタイミング攻撃の検出・防御など、セキュリティの問題に応用する研究をしています。

※イメージ画像

定理証明・制約解消アルゴリズム↗

プログラム検証・合成に欠かせない自動定理証明や、それに関連する制約解消アルゴリズムを研究しています。循環証明や不動点論理といった証明の体系を扱っています。

Voices先輩の声

評価・クチコミは、在籍している（していた）学生個人の経験に基づくもので、研究室の公式見解ではありません。クチコミの有無や件数は、研究室の評価を表すものではありません。

インタビューに協力いただいた学生に、内容にかかわらず謝礼（1,000円分のギフト）をお渡しすることがあります。