6月28日，应中科院深圳先进技术研究院数字所嵌入式软件系统研究中心方菱副研究员邀请，日本北陆先端科学技术大学院大学（Japan Advanced Institute of Science and Technology， JAIST）小川瑞史教授在深圳先进技术研究院进行学术交流，并作了题为Backend Tools for Code-level Formal Method的学术报告。

小川瑞史教授以系统验证的重要性和必要性为切入点，展示了他所领导的研究团队在形式化方法的理论研究和应用上所取得的成果，并从SAT/SMT工具和模型验证（Model Checking）两个方向详尽阐述了形式化方法（Formal Method）的基本理论。在本次报告中，小川教授讲述了两个形式化方法的应用实例，分别是程序模型中对于舍入/溢出（Roundoff/Overflow）错误的分析，和单线程的Java程序的上下文相关性解析。

讲座过程中，小川教授就模型验证与分析，形式化方法理论和应用等方面与科研人员及研究生进行了深入交流，现场气氛活跃。