On the Monniaux Problem in Abstract Interpretation

Nathanaël Fijalkow; Engel Lefaucheux; Pierre Ohlmann; Joël Ouaknine; Amaury Pouly; James Worrell

doi:10.1007/978-3-030-32304-2_9

On the Monniaux Problem in Abstract Interpretation

Nathanaël Fijalkow
, Engel Lefaucheux
, Pierre Ohlmann
, Joël Ouaknine
, Amaury Pouly
, James Worrell

École Polytechnique

The Alan Turing Institute
Max Planck Institute for Software Systems
Université Paris 7
University of Oxford

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Citations (Scopus)

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 (Forumala Presented)., and an abstract domain of invariants (Forumala Presented)., does there exist an inductive invariant (Forumala Presented). guaranteeing that program P meets its specification (Forumala Presented).. 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.

Original language	English
Title of host publication	Static Analysis - 26th International Symposium, SAS 2019, Proceedings
Editors	Bor-Yuh Evan Chang
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	162-180
Number of pages	19
ISBN (Print)	9783030323035
DOIs	https://doi.org/10.1007/978-3-030-32304-2_9
Publication status	Published - 1 Jan 2019
Event	26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal Duration: 8 Oct 2019 → 11 Oct 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11822 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
Country/Territory	Portugal
City	Porto
Period	8/10/19 → 11/10/19

Access to Document

10.1007/978-3-030-32304-2_9

Cite this

Fijalkow, N., Lefaucheux, E., Ohlmann, P., Ouaknine, J., Pouly, A., & Worrell, J. (2019). On the Monniaux Problem in Abstract Interpretation. In B.-Y. E. Chang (Ed.), Static Analysis - 26th International Symposium, SAS 2019, Proceedings (pp. 162-180). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11822 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-32304-2_9

Fijalkow, Nathanaël ; Lefaucheux, Engel ; Ohlmann, Pierre et al. / On the Monniaux Problem in Abstract Interpretation. Static Analysis - 26th International Symposium, SAS 2019, Proceedings. editor / Bor-Yuh Evan Chang. Springer Science and Business Media Deutschland GmbH, 2019. pp. 162-180 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{02340304913d4c159d057cd52e05c5c0,

title = "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 (Forumala Presented)., and an abstract domain of invariants (Forumala Presented)., does there exist an inductive invariant (Forumala Presented). guaranteeing that program P meets its specification (Forumala Presented).. 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.",

author = "Nathana{\"e}l Fijalkow and Engel Lefaucheux and Pierre Ohlmann and Jo{\"e}l Ouaknine and Amaury Pouly and James Worrell",

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 ; Conference date: 08-10-2019 Through 11-10-2019",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-32304-2\_9",

language = "English",

isbn = "9783030323035",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "162--180",

editor = "Chang, \{Bor-Yuh Evan\}",

booktitle = "Static Analysis - 26th International Symposium, SAS 2019, Proceedings",

}

Fijalkow, N, Lefaucheux, E, Ohlmann, P, Ouaknine, J, Pouly, A & Worrell, J 2019, On the Monniaux Problem in Abstract Interpretation. in B-YE Chang (ed.), Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11822 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 162-180, 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019, Porto, Portugal, 8/10/19. https://doi.org/10.1007/978-3-030-32304-2_9

On the Monniaux Problem in Abstract Interpretation. / Fijalkow, Nathanaël; Lefaucheux, Engel; Ohlmann, Pierre et al.
Static Analysis - 26th International Symposium, SAS 2019, Proceedings. ed. / Bor-Yuh Evan Chang. Springer Science and Business Media Deutschland GmbH, 2019. p. 162-180 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11822 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On the Monniaux Problem in Abstract Interpretation

AU - Fijalkow, Nathanaël

AU - Lefaucheux, Engel

AU - Ohlmann, Pierre

AU - Ouaknine, Joël

AU - Pouly, Amaury

AU - Worrell, James

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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 (Forumala Presented)., and an abstract domain of invariants (Forumala Presented)., does there exist an inductive invariant (Forumala Presented). guaranteeing that program P meets its specification (Forumala Presented).. 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.

AB - 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 (Forumala Presented)., and an abstract domain of invariants (Forumala Presented)., does there exist an inductive invariant (Forumala Presented). guaranteeing that program P meets its specification (Forumala Presented).. 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.

U2 - 10.1007/978-3-030-32304-2_9

DO - 10.1007/978-3-030-32304-2_9

M3 - Conference contribution

AN - SCOPUS:85075822979

SN - 9783030323035

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 162

EP - 180

BT - Static Analysis - 26th International Symposium, SAS 2019, Proceedings

A2 - Chang, Bor-Yuh Evan

PB - Springer Science and Business Media Deutschland GmbH

T2 - 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019

Y2 - 8 October 2019 through 11 October 2019

ER -

Fijalkow N, Lefaucheux E, Ohlmann P, Ouaknine J, Pouly A, Worrell J. On the Monniaux Problem in Abstract Interpretation. In Chang BYE, editor, Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Springer Science and Business Media Deutschland GmbH. 2019. p. 162-180. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-32304-2_9

On the Monniaux Problem in Abstract Interpretation

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this