On the Monniaux Problem in Abstract Interpretation

The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program P, a safety (e.g., non-reachability) specification \(\varphi \), and an abstract domain of invariants \(\mathcal {D}\), does there exist an inductive invariant \(\mathcal {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.