safety-critical

静的解析は飛行機が墜落しないことを証明できない。だが、もっと有益なことは証明できる。

抽象解釈はあらゆる可能なプログラム状態を過大近似する。抽象化の中でゼロ除算が到達不可能なら、実際のコードでも到達不可能である。以下に、その仕組みと限界を解説する。