创新形式化方法研究 保障计算机系统安全——上海交通大学符鸿飞特别副研究员

计算机系统越来越复杂，通过传统测试方法越来越难以覆盖足够多的系统执行路径。而形式化方法作为一个理论计算机科学的一个重要分支。为全覆盖的、自动化的系统正确性证明提供了一个行之有效的方法。上海交通大学电子信息与电气工程学院符鸿飞特别副研究员致力于形式化方法领域的研究，在形式化方法中的两个重要方向——模型检测和程序验证中都取得了一系列的创新成果。