Venue: 线上报告，腾讯会议 321 480 877

Abstract: 计算机程序中的许多性质和常见错误（如除零错、数组越界、算术溢出、计算精度缺陷等），与程序中数值型变量及其上的数值运算密切相关。针对数值代码开展自动分析，检测数值相关错误，验证相关性质，修复相关缺陷，对于提高计算机软件（尤其是数值计算密集型安全攸关软件）的可信性具有重要意义。本报告将围绕程序中数值相关性质与错误，介绍在基于抽象解释的数值程序分析与验证、基于数值近似的数值程序修复等方面的进展，以及在研究过程中碰到的数学问题。