Undecidability of Inferring Linear Integer Invariants

2018/12/03 by Shoham, Sharon
#FOS: Computer and information sciences #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.1812.01069

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.

Related

• Property Checking Without Inductive Invariants
• Invariant Checking for SMT-based Systems with Quantifiers
• One Henkin Quantifier in the empty vocabulary suffices for undecidability
• Invariants for Continuous Linear Dynamical Systems
• Decidable and undecidable problems about quantum automata