基于抽象解释的数值程序分析
Speaker
陈立前，国防科技大学
Time
2021-06-21 09:30:00 ~ 2021-06-21 10:30:00
Location
软件大楼专家楼1319会议室
Host
符鸿飞
Abstract
计算机程序中的许多性质和常见错误（如除零错、数组越界、算术溢出、计算精度缺陷等），与程序中数值型变量及其上的数值运算密切相关。针对数值代码开展自动分析，检测数值相关错误，验证相关性质，对于提高计算机软件（尤其是数值计算密集型安全攸关软件）的可信性具有重要意义。本报告将围绕程序中数值相关性质与错误，介绍在基于抽象解释的数值程序分析方面取得的进展，包括数值抽象域的设计与实现、数值不变式的自动生成、分析应用领域实际程序所遇到的问题和解决方法等。
Bio
陈立前，国防科技大学计算机学院副教授，主要从事程序分析与验证、抽象解释相关研究。在ACM/IEEE Transactions、POPL、FSE等期刊会议上发表论文多篇，获ACM SIGSOFT杰出论文奖（FSE 2020），出版教材译著3部。研究成果获省部级科技进步一等奖1项、二等奖1项。部分成果已在航天、国防等领域重大工程中应用。