On the Monniaux Problem in Abstract Interpretation
On the Monniaux Problem in Abstract Interpretation
复制标题
论抽象解释中的蒙尼奥问题
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
J. Worrell
中科院分区：
文献类型：
--
作者：
Nathanaël Fijalkow;Engel Lefaucheux;Pierre Ohlmann;Joël Ouaknine;Amaury Pouly;J. Worrell
粗略地说，抽象解释中的蒙尼奥问题询问以下问题是否可判定：给定一个程序 $P$、一个安全（emph{e.g.}、不可达）规范 $varphi$ 和一个不变量抽象域 $mathcal{D}$，$mathcal{D}$ 中是否存在一个归纳不变量 $I$ 来保证程序 $P$ 满足其规范 $varphi$。蒙尼奥问题当然是由人们所考虑的程序类别和不变域参数化的。在本文中，我们证明蒙尼奥问题对于无保护仿射程序和半线性不变量（多面体并集）是不可判定的。此外，我们证明了在简单线性循环的重要特殊情况下可判定性得到了恢复。
The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program $P$, a safety (emph{e.g.}, non-reachability) specification $varphi$, and an abstract domain of invariants $mathcal{D}$, does there exist an inductive invariant $I$ in $mathcal{D}$ guaranteeing that program $P$ meets its specification $varphi$. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this paper, we show that the Monniaux Problem is undecidable for unguarded affine programs and semilinear invariants (unions of polyhedra). Moreover, we show that decidability is recovered in the important special case of simple linear loops.