理论上来说，静态分析问题是不可判定的（undecidable）；实际上，可以通过过度近似（over-approximation）来得到准确的单边答案，也就是可以保证假阴性和假阳性不会同时出现。

“程序状态”可以定义为：$\{label, store\_mapping\}$,也就是程序执行的位点与各个变量的值。

使 $U$ 为程序状态的全集，$B$ 为有问题的状态集合，$R$ 为可到达的状态集合。如果 $R$ 与 $B$ 不相交，那么说明该程序无法到达有问题的状态，故而没有问题。而如果有相交，则程序有问题（有 bug）。

$R$ 是不可判定的，因此无法通过静态分析确定程序是否有问题。但是可以通过计算 $R$ 的超集来“过度近似” $R$。这样，对于发现的问题，可能会出现假阳性；但如果没发现问题，可以确定肯定没有问题。