寺内研究室

About关于研究室

以实现无bug的软件为目标。

寺内研究室研究编程语言领域。
主要研究自动确认程序是否按规约运行的“程序验证”，以及根据规约自动生成正确程序的“程序合成”。
该研究室还研究将这些技术应用于信息泄露、时序攻击等安全问题。
同时也致力于类型系统、数理逻辑、形式语言理论等支撑这些技术的基础理论研究。

Research研究课题

寺内研究室利用计算机算法，以机械方式验证程序的正确性，并以机械方式合成正确的程序，从而提高软件的可靠性。该研究室重视类型系统、数理逻辑等以理论为根基的方法。

※示意图

程序验证↗

通过分析程序代码，验证其是否按规约运行的研究。该研究室致力于高效验证包含高阶函数等的高级语言程序的技术。

※示意图

程序合成↗

根据规约或输入输出示例，自动生成正确程序的研究。研究内容包括自动合成能抵御侧信道攻击的代码以及安全的正则表达式的方法。

※示意图

在安全领域的应用↗

将程序验证与合成技术应用于机密信息泄露、时序攻击的检测与防御等安全问题的研究。

※示意图

定理证明・约束求解算法↗

研究程序验证与合成不可或缺的自动定理证明，以及与之相关的约束求解算法。研究对象包括循环证明、不动点逻辑等证明体系。

Voices学长学姐的评价

评价基于在读（或曾在读）学生的个人经历，不代表研究室官方观点。评价的有无或数量不代表对研究室的评价。

对于接受采访的学生，无论内容如何，我们可能会赠送谢礼（价值1,000日元的礼品）。