Questions: Invariant Generation

Question 1

Why is invariant generation considered the bottleneck of automated deductive verification?

• A. Because invariants are only needed for recursive functions, which are uncommon
• B. Because for straight-line code and conditionals, weakest precondition computation is entirely mechanical, but loops require an invariant that cannot be derived mechanically in general. The invariant must be both preserved by the loop body (inductive) and strong enough to imply the postcondition upon exit
• C. Because invariant generation requires exponential time in all cases
• D. Because modern SMT solvers cannot check invariant candidates

Answer: (B)

Verification of straight-line code is fully automated by weakest precondition computation. Loops are the obstacle: the wp calculus needs a loop invariant to cut the loop, and finding invariants is undecidable in general. The invariant must satisfy two constraints simultaneously: (1) it is preserved by one iteration of the loop body (inductiveness), and (2) combined with the loop exit condition, it implies the postcondition (sufficiency). Balancing these — strong enough but not too strong — is the creative challenge that automation aims to solve.

Question 2

An invariant candidate I for a loop is valid if it satisfies three conditions: (1) I holds on loop entry, (2) I is preserved by the loop body, and (3) I combined with the exit condition implies the postcondition.

• T. True
• F. False

Answer: True

These are the three verification conditions for a loop invariant in Hoare logic. (1) Initiation: the precondition implies I before the loop starts. (2) Consecution (inductiveness): {I AND loop_condition} body {I} — the invariant is maintained by each iteration. (3) Sufficiency: I AND NOT loop_condition implies the postcondition. All three must hold. The invariant 'true' always satisfies (1) and (2) but is typically too weak for (3). The art is finding an I that is strong enough for (3) while still satisfying (2).

Question 3

Describe how abstract interpretation can be used to generate loop invariants, and what determines the precision of the generated invariants.

Model answer: Abstract interpretation computes a fixed point of the abstract transfer function for the loop body, starting from the abstract initial state. The fixed point IS the loop invariant (in the abstract domain). Widening forces convergence when the domain has infinite ascending chains. The precision of the invariant depends on the abstract domain: interval analysis generates bounds (x in [0, 100]), octagon analysis generates relational constraints (+/-x +/- y <= c), and polyhedra analysis generates arbitrary linear constraints. Richer domains yield stronger invariants but at higher computational cost.

This is the most principled approach to invariant generation. The abstract domain determines what kinds of invariants can be expressed. If the true invariant is 'x + y <= n', interval analysis cannot discover it (it only tracks individual variables), but octagon analysis can. If the invariant involves nonlinear relationships, all these domains fail, and you need polynomial invariants or template-based approaches. Choosing the right domain for the target property is the key engineering decision.