Undecidable to find polyhedral invariants in linear programs
The existence of polyhedral invariants is undecidable for linear systems
Logic in Computer Science
Summary
Sometimes computer programs need special rules, called invariants, to prove certain parts of the program can never be reached. This paper shows that when programs use only simple math with whole or fractional numbers, it is impossible to always decide if such rules exist. The researchers used a known hard problem involving simple machines with two counters to prove this. This means there are limits to what automatic tools can verify about some programs.
What this means in practice
- •For program verification engineers: Recognize limits in automated analysis tools when searching for polyhedral invariants in linear arithmetic programs, guiding tool design choices.
- •For software model checkers: Avoid relying solely on polyhedral invariant detection for reachability proofs in systems modeled by linear arithmetic, due to undecidability.
A theory result. No direct application yet.
Authors
David Monniaux
Abstract
The existence of polyhedral inductive invariants suitable for proving that a given control location is unreachable is undecidable for programs using only linear arithmetic over Z or Q, by reduction from 2-counter machines.