Undecidability of Inferring Linear Integer Invariants
Sharon Shoham
TL;DR
This paper proves that it is impossible to algorithmically determine the existence of linear integer invariants in certain logical systems, highlighting fundamental limits in automated reasoning.
Contribution
It establishes the undecidability of inferring linear integer invariants within quantifier-free linear integer arithmetic.
Findings
Undecidability of invariant inference in QFLIA
Implications for automated verification tools
Limits on automated reasoning in integer systems
Abstract
We show that the problem of determining the existence of an inductive invariant in the language of quantifier free linear integer arithmetic (QFLIA) is undecidable, even for transition systems and safety properties expressed in QFLIA.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Software Reliability and Analysis Research