safety-critical

静态分析无法证明你的飞机不会坠毁。但它能证明一些更有用的东西。

抽象解释会对每一种可能的程序状态进行过度近似。如果除零错误在抽象中不可达，那它在真实代码中就不可达。以下是它的工作原理以及它的局限性。