On the Monniaux problem in abstract interpretation

DOI10.1007/978-3-030-32304-2_9MaRDI QIDQ6536286zbMATHFDO

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

Publication date 19 April 2024

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Decidability of inferring inductive invariants
• Inadequacy of computable loop invariants
• Deciding program properties via complete abstractions on bounded domains
• Abstract interpretation of programs as Markov decision processes
• scientific article; zbMATH DE number 2090849

Cites work

• scientific article; zbMATH DE number 435565 (Why is no real title available?)
• Affine relationships among variables of a program
• Analyzing program analyses
• Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• Donut domains: efficient non-convex domains for abstract interpretation
• Extending constraint-only representation of polyhedra with Boolean constraints
• Making abstract interpretations complete
• On the decidability of the existence of polyhedral invariants in transition systems
• Polynomial Invariants for Affine Programs
• Polynomial-time algorithm for the orbit problem
• Semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• Static Analysis
• The Complexity of theA B CProblem
• Undecidability of infinite post correspondence problem for instances of Size 9
• Verification, Model Checking, and Abstract Interpretation
• Why does Astrée scale up?

Cited in

(1)

• Porous invariants for linear systems

This page was built for publication: On the Monniaux problem in abstract interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536286)