Abstract Invariant Generator

When → invariant-inference (which works from concrete traces) can't find the invariant, abstract interpretation can. It over-approximates: instead of tracking exact values, track which region of a chosen domain the values are in.

Abstract domains — pick by invariant shape

Start cheap. Intervals catch 80% of array-bounds invariants. Octagons catch most two-pointer patterns. Polyhedra are for when you actually need a weird linear relationship.

The algorithm (fixpoint iteration)

1. Abstract the initial state. i = 0 → in intervals: i ∈ [0, 0].
2. Abstract the transition. i := i + 1 on [a, b] → [a+1, b+1].
3. Join at loop head. Union the incoming abstract states: [0,0] ⊔ [1,1] = [0,1].
4. Iterate until fixpoint. The loop stabilizes → that's your invariant.
5. Widen if it doesn't stabilize. [0,1] ⊔ [0,2] ⊔ [0,3] ⊔ ... → widen to [0, +∞). Then narrow: apply the loop guard i < n to get [0, n-1].

Worked example — interval domain

Code:

int i = 0, j = n;
while (i < j) {
    i++;
    j--;
}
// invariant at loop head? need: 0 ≤ i, j ≤ n, and relationship between i and j

Interval abstraction:

Interval invariant: 0 ≤ i ≤ n ∧ 0 ≤ j ≤ n. True but weak — doesn't capture i + j = n.

Octagon domain (tracks ±x ± y ≤ c):

Initial: i + j = n (since i=0, j=n). Transition: i' = i+1, j' = j-1 → i' + j' = i + j = n. Preserved. Octagon finds i + j = n (as i+j ≤ n ∧ -(i+j) ≤ -n).

Lesson: Intervals are per-variable; they can't see i + j = n. For relational invariants, you need a relational domain.

Choosing the domain

1. Look at the postcondition you're trying to prove. What shape is it?
   • Single-var bound → intervals suffice.
   • Two-var comparison (i ≤ j) → octagons.
   • Three+ var linear → polyhedra.
   • Divisibility → congruence.
2. Run with the cheapest domain that could express it.
3. If the result is too weak (e.g., [-∞, +∞]), the domain can't express the invariant — upgrade.

Do not

• Do not start with polyhedra. They're exponentially expensive. Intervals → octagons → polyhedra.
• Do not forget to narrow after widening. Widening alone gives [0, +∞) — useless. The guard narrows it back.
• Do not expect abstract interpretation to find nonlinear invariants. i*i ≤ n — none of these domains can express it. You need a polynomial domain or template-based search.
• Do not trust an invariant without checking it's inductive. Abstract interpretation is sound (no false invariants) — but double-check by plugging it back into the verifier.

Output format

## Domain
<interval | octagon | polyhedra | congruence> — <why this domain>

## Fixpoint iteration
<table: iteration → abstract state>

## Invariant
<the stabilized abstract state, written as a logical formula>

## Strength check
Sufficient for the postcondition? <yes | no — need stronger domain: which>