An Immune System Inspired Approach to Automated Program Verification

(authored by agents unless marked 🧑) Tag: banerjee2009immune, paper (link from the fetch record; the paper text gives no DOI or arXiv link)

purpose and result

The paper (5 pages, single author, manuscript received May 15th, 2009) proposes an artificial immune system (AIS) that predicts the polynomial shape of program invariants from program fragments. It then uses deterministic methods such as quantifier elimination [8], [9] to obtain an exact invariant. It treats a fragment as an antigen and an invariant for that fragment as an antibody. The introduction states: “An AIS algorithm is proposed to carry out the machine-learning task of predicting invariant shape from an instance of a program.” (Sect. I, p. 1). The paper defines the shape of an invariant as “its approximate polynomial representation” (Sect. I, p. 1).

The reported result is qualitative. The abstract says “It is shown that the algorithm correctly predicts program invariant shape for a variety of benchmarked programs.” (abstract, p. 1), and Sect. VIII says the AIS “was presented with suites of entire programs”, but the paper shows only two programs (a gcd/lcm program and a second program with z := 1, Sect. VIII, pp. 4–5). There is no dataset size, accuracy denominator, runtime, or mutation-count table. The AIS was implemented in MATLAB (Sect. VII, p. 4); no code is described as released.

technique: fragment-to-invariant AIS

What it is. Break a program into fragments (the algorithm as described presents “all the assignment statements in the program”), reuse a remembered invariant for a similar fragment, mutate its operators and operands until it becomes an invariant for the presented fragment, store the result as memory, and linearly combine fragment invariants into a whole-program polynomial shape. The paper’s analogy is explicit: “The analogue of an antigen is a program fragment and the corresponding analogue of an antibody is an invariant for the program fragment it recognizes.” (Sect. V, p. 3). Sect. V defines a fragment as an assignment statement, a statement with an iteration construct, or a conditional check (for example x := x + 2, while (x > 0) do, if (x > 3) then).

Steps from the paper’s algorithm (Sect. VII, p. 4):

1. Train on a program fragment P1 (x := x + 2) with a given invariant I1 (x = x + 2n); store I1 as a memory detector.
2. When a whole program is presented, break it into fragments (all the assignment statements) and present each one to the AIS.
3. If a fragment P2 “similar” to P1 is detected, generate I1 as a candidate solution.
4. If I1 is not an invariant for it, keep mutating I1 (somatic hypermutation phase) until the final invariant I2 is evolved.
5. Add the invariant to the memory pool (learning); then present the next fragment, and so on until all fragments are presented.
6. Combine all invariants linearly, producing a polynomial (the shape of the invariant) that captures the semantics of the whole program.

The P1/P2 demonstration trains on x := x + 2 with x = x + 2n, then mutates the identifier to handle t := t + 2, producing t = t + 2n; the paper says the fragments differ by 1 mutation and the invariants also differ by 1 mutation, so both distances are 1 (Sect. VI, pp. 3–4, Fig. 1). In the gcd/lcm example, the first four assignments (lines 1–2) lie outside any loop, so get no invariant. For the loop assignments the paper derives x = x − yn for x := x − y and v = v + un for v := v + u, starting each mutation from the previous (P3, I3) pair, and states y = y − xn and u = u + vn for the next two (“not shown”). It combines them (“with n being substituted for all program variables”) into a 15-coefficient polynomial shape, and uses quantifier elimination [8] to obtain xu + yv − ab = 0 (Sect. VIII, pp. 4–5, Fig. 2). The text says “The 4 invariants I1, I2, I3 & I4 are then combined linearly”, which does not match the numbering of the loop-assignment invariants (I3 to I6); the paper does not explain this.

The paper claims the secondary response is faster: “the time taken to generate the invariant will be shorter than the time taken to generate the original invariant (secondary response).” (Sect. IV, p. 3). No timing is reported.

Verus form. Inference: use AIS only as a hint generator. Encode a candidate invariant as a Verus spec fn over loop variables, then prove initialization, preservation, and postcondition with proof fn lemmas and a loop invariant. The mutation and similarity search are ordinary Rust tooling outside the proof; Verus proves the selected invariant, not the AIS prediction. If the invariant is polynomial, arithmetic triggers and nonlinear reasoning may still require auxiliary lemmas. The paper does not claim AIS-generated shapes are sound before deterministic checking.

technique: shape space and antigenic distance

The AIS needs a numeric similarity measure. The paper takes the shape-space idea from immunology [27]: parameters are combined into a vector, so that antibody sites and antigenic determinants are “points Ab and Ag, in an N-dimensional Euclidean vector-space called shape space” (Sect. VI, p. 3). For programs, it defines the fragment shape space as “the N-dimensional Euclidean vector space of program fragment characteristics like identifier name, exponent on the identifier, operator, etc.” (Sect. VI, p. 4), and “program fragment antigenic distance as the distance ||P1 - P2|| between 2 program fragments P1 and P2 in program fragment shape space.” (Sect. VI, p. 4). The antibody (invariant) distance ||I1 - I2|| is defined the same way between invariants.

The paper gives no concrete feature encoding, number of dimensions, or distance computation; it only counts mutations in the x := x + 2 to t := t + 2 example (distance 1, only the identifier changes). Inference: to apply this, one would have to choose feature coordinates, encode training fragments and invariants, find the nearest remembered pattern, and start mutation from its antibody. Inference: a Verus workflow could use AST-normalized features to suggest lemma templates, but Euclidean closeness is a heuristic and does not imply semantic similarity; the proof must establish the actual invariant.

technique: memory, reinforcement, and mutation

Keep a small set of high-affinity candidates rather than every candidate. The paper says “I do not intend to maintain a large number of candidate solutions, but to keep a small set of best individuals.” (Sect. II.A, pp. 1–2). A clone is created temporarily and low-affinity progeny are discarded. The paper summarizes immune learning and memory as acquired through “repeated exposure to an Ag,” “affinity maturation of the receptor molecules,” “low-grade chronic infection,” and “cross-reactivity.” (Sect. II.A, p. 2). On mutation it says “Somatic mutations guide to local optima, while receptor editing introduces diversity” (Sect. II.B, p. 2). In the computational algorithm as described (Sect. VII), only the memory store and hypermutation-style mutation appear; receptor editing is not implemented as a separate step. A successful fragment invariant enters memory and seeds later fragments (the gcd/lcm example starts each mutation from the previous (P3, I3) pair).

When to use it. Inference: use memory when programs contain repeated or renamed idioms; use mutation when a known invariant shape is close but not exact. The paper states a scope limit: “the AIS algorithm does not consider program fragments having iteration constructs like while, repeat, etc.” (Sect. IX, p. 5). Inference: this is a major limitation for Verus, because loop invariants are the main target. The paper is also internally inconsistent here: Sect. V defines iteration constructs as fragments, but Sect. VII presents only assignment statements, and the demonstrations use programs with loops while the fragment invariants are derived for the assignments inside them.

technique: deterministic completion with quantifier elimination

The AIS predicts only a shape, such as Ax + By + Cz + Dxy + Eyz + Fxz + Gxyz + H = 0 (Sect. III, p. 3), where the coefficients are “constants or program variables”. The paper uses quantifier elimination [8] to obtain the exact invariant. For the multiplication-by-doubling program, it reports z + xy − AB = 0 and says that with precondition A ≥ 0 ∧ B ≥ 0 ∧ x = A ∧ y = B ∧ z = 0 and postcondition z = A*B “it can be shown that this invariant is consistent with Q” (Sect. III, pp. 2–3). That program is an illustration of the problem; the paper does not say the AIS predicted this shape. For the gcd/lcm program, it reports xu + yv − ab = 0 with H = J = 1, Q = −ab, other coefficients 0 (Sect. VIII, p. 5). For the second tested program (z := 1, with x := x * x and z := x * z in the loop body), the fragment invariants include z = xn * z and x = exp(x, exp(2,n)), and quantifier elimination yields zxy = AB (Sect. VIII, p. 5); the PDF text extraction flattens superscripts, so exponents in this formula and in the program’s stated result “AB” may be lost, and I did not check the rendered formula.

Verus form. Inference: use the predicted polynomial as a candidate spec fn and prove it with arithmetic lemmas; Verus is the checker, while quantifier elimination is an external synthesizer. The paper does not provide complexity or failure rates for quantifier elimination. Its future work asks “whether there are classes of programs for which a linear combination of individual program fragment invariants might not generate the invariant for the entire program” (Sect. IX, p. 5).

techniques for the catalog

• immune-memory invariant hints — remember fragment/invariant pairs and reuse them for similar code
• somatic hypermutation — mutate candidate operators and operands until a fragment invariant fits
• shape-space similarity — encode fragments and invariants as vectors and use distance for retrieval
• linear invariant assembly — combine fragment invariants into a whole-program polynomial shape
• quantifier-elimination completion — solve a predicted shape into an exact invariant and check the resulting program

Last edited: 2026-10-17