Undecidability of Inferring Linear Integer Invariants
Programming Languages
2018-12-10 v2
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.
Cite
@article{arxiv.1812.01069,
title = {Undecidability of Inferring Linear Integer Invariants},
author = {Sharon Shoham},
journal= {arXiv preprint arXiv:1812.01069},
year = {2018}
}