Conference item
On the Monniaux Problem in abstract interpretation
- Abstract:
- 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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 889.5KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-030-32304-2_9
Authors
- Publisher:
- Springer
- Host title:
- Lecture Notes in Computer Science
- Journal:
- Lecture Notes in Computer Science More from this journal
- Volume:
- 11822
- Pages:
- 162-180
- Publication date:
- 2019-10-02
- Acceptance date:
- 2019-06-14
- DOI:
- Pubs id:
-
pubs:1040501
- UUID:
-
uuid:0b921a93-1808-4ffc-aa47-cc9cab4b6ba0
- Local pid:
-
pubs:1040501
- Source identifiers:
-
1040501
- Deposit date:
-
2019-08-09
- ARK identifier:
Terms of use
- Copyright date:
- 2019
- Notes:
- Conference paper from the 26th Static Analysis Symposium, October 8-11, 2019 Porto, Portugal. This is the accepted manuscript version of the article. The final version is available online from Springer at: https://doi.org/10.1007/978-3-030-32304-2_9
If you are the owner of this record, you can report an update to it here: Report update to this record