一种通过抽象对程序语义上的特定性质进行分析的方法。通常为静态分析、使用上近似（may analysis），即存在误报/假阳性。程序分析领域一般把这种情况称为可靠的（sound），不过如果按照逻辑学的观点，这应该是完备。与之相对的使用下近似的分析为 must analysis。
Static program analysis is the art of reasoning about the behavior of computer programs without actually running them.
可以针对特定的缺陷进行分析，也可以被用作编译器优化/形式化验证工具的组件。