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 φ, and
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 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.
Proceedings of SAS 19, LNCS 11822, 2019. 37 pages.
© 2019 Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann,
Joël Ouaknine, Amaury Pouly, and James Worrell.