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
specification φ, and an abstract domain of invariants D, does there exist
an inductive invariant I in D guaranteeing that program P meets its
specification φ. The Monniaux Problem is of course parameterised by
the classes of programs and invariant domains that one considers. In
this talk, I’ll present a select overview and survey of works on this problem,
and discuss some recent results for semilinear invariants for unguarded
affine programs.