On the 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 (e.g., non-reachability) specification ϕ, and an abstract domain of invariants D, does there exist an inductive invariant I in D guaranteeing that program...
Main Authors: | Fijalkow, N, Lefaucheux, E, Ohlmann, P, Ouaknine, J, Pouly, A, Worrell, J |
---|---|
Format: | Conference item |
Published: |
Springer
2019
|
Similar Items
-
Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
by: Fijalkow, N, et al.
Published: (2017) -
Semialgebraic invariant synthesis for the Kannan-Lipton Orbit Problem
by: Fijalkow, N, et al.
Published: (2017) -
Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
by: Fijalkow, N, et al.
Published: (2019) -
On the decidability of reachability in linear time-invariant systems
by: Fijalkow, N, et al.
Published: (2019) -
The 2-dimensional constraint loop problem is decidable
by: Guilmant, Q, et al.
Published: (2024)