Monniaux Problem in Abstract Interpretation

Prelegent(ci)

Engel Lefaucheux

Afiliacja

MPI SWS

Termin

1 kwietnia 2020 14:15

Informacje na temat wydarzenia

Online seminar

Seminarium

Seminarium „Teoria automatów”

---

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.

---