2月23日下午4时，在逸夫楼C座314，公司计算机科学系郭曦副教授做了题为“符号执行（Symbolic Execution）40年：回顾，挑战，展望”的学术报告。学院王建勇、翟瑞芳、刘善梅老师，员工代表等聆听了报告。

该报告首先从软件安全的角度展开，指出检测软件中的安全问题成为软件工程、信息安全等领域的研究热点。在安全检测方面，基于源代码的静态分析是应用最为广泛的方法，其中的符号执行的分析方法是时下最为主流的分析方法。接下来，报告介绍了符号执行诞生的背景，着重介绍了该方法的思路和原理，并通过两个具体的符号执行工具DART和CUTE来分析符号执行的工作过程，并分析了该方法相对于传统分析方法的巨大优势。随后报告介绍了符号执行在40年的发展过程中存在的几个主要挑战，例如状态空间爆炸，约束求解能力以及复杂语义建模等，以及相应的解决思路。报告最后对符号执行的发展趋势做了相应的分析。

报告结束，郭曦对与会人员提出的问题进行了深入的探讨和交流。