一句话：针对数值抽象域实现难以测试的问题，研究自动测试方法以保障静态分析的可靠性与精度。
静态程序分析常用于代码优化与安全漏洞检测，其结论要可信，分析必须可靠（不产生假阴性）且精确（假阳性少）。尽管可以在设计层面证明静态分析的性质，但要保证具体实现的可靠性与精确性仍很困难：复杂算法与精细优化使静态分析器难以实现和测试。本文关注数值抽象域这一静态分析核心组件的实现测试，研究自动测试方法，以发现实现中的缺陷并提升分析器可信度。给出的英文摘要未展开具体测试生成技术、实验对象与结果，因此无法概述其方法细节与量化评估；其核心问题是如何对数值抽象域实现进行自动化、有效的测试。
Static program analyses are routinely applied as the basis of code optimizations and to detect safety and security issues in software systems. For their results to be reliable, static analyses should be sound (i.e., should not produce false negatives) and precise (i.e., should report a low number of false positives). Even though it is possible to prove properties of the design of a static analysis, ensuring soundness and precision for its implementation is challenging. Complex algorithms and sophisticated optimizations make static analyzers difficult to implement and test.
DOI 原文 ·
@inproceedings{paperbot4755,
title = {Automatically testing implementations of numerical abstract domains},
author = {Alexandra Bugariu and Valentin Wüstholz and Maria Christakis and Peter Müller},
booktitle = {ASE},
year = {2018},
doi = {10.1145/3238147.3240464}
}