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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

4 Citations (Scopus)

Résumé

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.

langue originale	Anglais
titre	Static Analysis - 26th International Symposium, SAS 2019, Proceedings
rédacteurs en chef	Bor-Yuh Evan Chang
Editeur	Springer Science and Business Media Deutschland GmbH
Pages	162-180
Nombre de pages	19
ISBN (imprimé)	9783030323035
Les DOIs	https://doi.org/10.1007/978-3-030-32304-2_9
état	Publié - 1 janv. 2019
Evénement	26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal Durée: 8 oct. 2019 → 11 oct. 2019

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11822 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
Pays/Territoire	Portugal
La ville	Porto
période	8/10/19 → 11/10/19

Accès au document

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

Contient cette citation

Fijalkow, N., Lefaucheux, E., Ohlmann, P., Ouaknine, J., Pouly, A., & Worrell, J. (2019). On the Monniaux Problem in Abstract Interpretation. Dans B.-Y. E. Chang (Ed.), Static Analysis - 26th International Symposium, SAS 2019, Proceedings (p. 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. Editeur / 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)).

@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. Dans 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, p. 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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. Dans Chang BYE, Editeur, 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

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation