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
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 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.
PDF
© 2019 Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann,
Joël Ouaknine, Amaury Pouly, and James Worrell.