抽象解释静态分析中的完备性：个人观点
编程语言
2024-12-11 v3
摘要
基于抽象解释的静态分析通常被设计为“可靠（sound）”的，即它不应声称建立不成立的属性——换言之，不对可能的缺陷提供“假阴性”。一个更少见的要求是它应是“完备（complete）”的，意味着若某些属性成立，它应能够推断出来。本文描述了多年来我所遇到的与完备性相关的若干实际问题和疑问。
引用
@article{arxiv.2211.09572,
title = {Completeness in static analysis by abstract interpretation, a personal point of view},
author = {David Monniaux},
journal= {arXiv preprint arXiv:2211.09572},
year = {2024}
}