&gt; The problem of array overflow&#x2F;underflow is undecidable in the general case.<p>Obviously.<p>&gt; Various verification techniques (like SMT solvers) can only prove some usages, but not all.<p>Turns out this is good enough for most cases. Verifying 80% of your array index manipulations is better than verifying none of it.