2019年1月更新

寺内研究室 教授 寺内多智弘

当研究室を希望する方へ

プログラミング言語分野の研究を行っています。特に、「正しいソフトウェアの開発」を目標とし、プログラム検証、プログラム合成などの研究を行っています。

研究概要

近年、コンピュータソフトウェアは生活のいたるところで使用されており、ソフトウェアの不具合は大きな社会的課題となっています。また、テスト実行など従来のソフトウェア開発手法では、複雑化を増すソフトウェアの品質を保証することが難しくなっています。そこで、コンピュータアルゴリズムにより正式かつ機械的にプログラムの正しさを検証したり正しいプログラムを合成することにより、ソフトウェアの信頼性を向上しよう、というのが研究のねらいです。特に、本研究室では、自動定理証明・型システムなど数理論理学・理論計算機科学に根ざした手法の研究を行っています。

お知らせ

早稲田大学基幹理工学部のClose Upにバグのないソフトウェアを目指して:近年のプログラム検証研究の動向という記事を寄稿しました。そちらも参考にしてください。

研究室の論文は寺内のホームページから参照してください。

近年の研究テーマ

プログラム検証

プログラム検証とは、プログラムコードを解析し、プログラムが仕様通り動作するか検証することです。近年、SMTソルバなど定理証明技術の著しい進歩もあり、「ソフトウェアモデル検査」と呼ばれる高精度な自動プログラム検証手法が注目されています。プログラム検証の研究には、扱える言語機能の拡張(例えば、高階関数の扱い)など様々な課題があります。当研究室では、高階関数や再帰データ構造などを含む高レベル言語で記述されたプログラムを効率よく検証する技術を研究しています。

プログラム合成

仕様や入出力例などから自動的にプログラムを生成することをプログラム合成と呼びます。プログラム検証と同様、定理証明など数理論理のアイデアを用いることが多く、これら技術の発展により急速に研究が進んでいます。当研究室では、SMTソルバを分割統治法的に使いサイドチャネル攻撃に対する耐タンパコードを合成する手法を研究しています。また、テスト実行に基づいたプログラム修復なども研究しています。

情報セキュリティへの応用

プログラム検証・合成などプログラミング言語研究の技術を情報セキュリティに応用することができます。上記のサイドチャネル攻撃に対する耐タンパコードを合成はその一例です。当研究室では、上記の耐タンパコード合成の他、機密情報漏洩の検出・防衛に関する研究やタイミング攻撃の検出・防衛に関する研究などを行っています。

自動定理証明および制約解消アルゴリズムの研究

プログラミング言語研究には、定理証明など数理論理に関する理論・アルゴリズムが深くかかわります。定理証明は論理式の真偽性を自動的に判定するアルゴリズムです。上記の通りプログラム検証・合成に不可欠な技術であり、当研究室でも定理証明および密接に関連する制約解消アルゴリズムの研究を行っています。特に、近年は、循環証明(cyclic proof)という帰納法を定式化する体系を用いて分離論理(separation logic)というプログラムが扱うデータ構造に関する論理を効率よく定理証明アルゴリズムや不動点論理(fixpoint logic)に対する定理証明アルゴリズムなどを研究しています。

先進的型システムの研究

型システムは、型エラーが実行時に起こらないことを保証し、Javaなど多くの プログラミング言語で使われるなど、正しいプログラム開発の重要な一端を担っ ています。さらに、まだ研究段階の依存型(dependent types)、交差型 (intersection types)や型とエフェクト(type and effect)など、より精密か つ柔軟な型システムもあり、近年も活発に研究されています。当研究室でもこ れら先進的型システムについての研究を行っています。

分野キーワード

プログラミング言語   数理論理   ソフトウェア工学   情報セキュリティ   プログラム検証   プログラム合成   自動定理証明   型システム