Questions: Abstract Interpretation

Question 1

An abstract interpretation using the sign domain reports that variable x is '+' (positive) at a program point. What does this guarantee about the concrete program?

• A. x is always exactly 1 at that point
• B. x is positive in every possible concrete execution reaching that point
• C. x is positive in at least one concrete execution reaching that point
• D. Nothing — abstract interpretation results are only approximations

Answer: (B)

The soundness of abstract interpretation guarantees that abstract values over-approximate all possible concrete values. If the abstract value is '+', then in every concrete execution that reaches that program point, x must be positive. The analysis might fail to determine the sign (returning 'top' = unknown) but will never claim '+' if x could be zero or negative in any execution. This is what 'sound over-approximation' means: the abstract domain contains all concrete possibilities.

Question 2

Widening is needed in abstract interpretation to guarantee termination when the abstract domain has infinite ascending chains.

• T. True
• F. False

Answer: True

Abstract interpretation computes loop invariants by iterating the abstract transfer function until a fixed point. If the abstract domain has infinite ascending chains (e.g., intervals [0,1], [0,2], [0,3], ... growing without bound), naive iteration may never converge. Widening is an operator that deliberately over-approximates the iteration to force convergence: instead of computing the exact next abstract value, it jumps to a safe over-approximation (e.g., [0, +infinity]). This guarantees termination at the cost of precision. Narrowing can subsequently recover some lost precision.

Question 3

Explain the difference between soundness and completeness in the context of abstract interpretation, and which property abstract interpretation guarantees.

Model answer: Soundness means the analysis never misses a real error — if a property holds in the abstract, it holds concretely. Completeness means the analysis never reports false alarms — every abstract alarm corresponds to a real error. Abstract interpretation guarantees soundness but NOT completeness. It may report false alarms (flagging safe code as potentially erroneous) because the abstraction loses information. The analysis says 'I cannot prove this is safe' rather than 'this is definitely buggy.'

This asymmetry is deliberate and fundamental. By Rice's theorem, no analysis can be both sound and complete for non-trivial program properties. Abstract interpretation chooses soundness (never miss a bug) and accepts the consequence of potential false alarms. The choice of abstract domain controls the precision-cost tradeoff: richer domains (polyhedra, octagons) produce fewer false alarms but are more expensive to compute than simpler domains (intervals, signs).