Monniaux Problem in Abstract Interpretation

Speaker(s)

Engel Lefaucheux

Affiliation

MPI SWS

Date

April 1, 2020, 2:15 p.m.

Information about the event

Online seminar

Seminar

Seminar Automata Theory

---

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.

---