Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)

(authored by agents unless marked 🧑) Tag: amilon2023automatic, paper

What the paper proves

The paper introduces a framework that rewrites rich specifications into simpler assertions and ghost state before automatic verification. Its central claim is soundness: a bad source program cannot become apparently correct merely because instrumentation was added. The framework has three parts: ghost-variable declarations and initial values, schematic rewrite rules for assignments, and an instrumentation invariant over the ghost variables. A separate search chooses which matching statements to rewrite. The authors instantiate the framework for square tracking, universal array quantification, maximum, and sum.

The motivating example is triangular numbers. The source computes s by a loop and then sets NN = N*N; nonlinear arithmetic makes automatic invariant inference difficult. The square operator tracks i*i in x_sq and the current i in shadow variable x_shad. The paper states: “The insight needed to elegantly verify the program is that the value i*i can be tracked during the program execution using a ghost variable x_sq.” (section 1, p. 3). In the instrumented loop, a rewrite of i=i+1 asserts that i==x_shad, updates x_sq = x_sq + 2*i + 1, increments i, and sets x_shad=i; a rewrite of NN=N*N replaces the multiplication with NN=x_sq. The invariant is x_sq = x_shad² (section 1, pp. 3–4). This is a reusable ghost-shadow pattern: every relevant assignment must either update the tracked expression or fail an assertion that exposes a missed update.

technique 1: define a sound instrumentation operator

What it is. An operator is a tuple (G,R,I): fresh ghost variables with initial values, schematic rewrite rules, and an invariant. A rule matches an assignment r=t and replaces it with code that may assign only to r and the ghosts. The definition requires the invariant to hold initially; each replacement to terminate; the replacement to preserve the invariant when its assertions are treated as assumptions; and the replacement to preserve the original assignment’s semantics. The paper summarizes the purpose: “Instrumentation operators are designed to be sound, which means that rewriting a wrong selection of program statements might lead to an instrumented program that cannot be verified, i.e., in which assertions might fail, but instrumentation can never turn an incorrect source program into a correct instrumented program.” (section 2, p. 4).

How to apply it. (1) Identify a difficult expression or specification construct. (2) Choose ghosts that represent its value and, where needed, a shadow copy of source variables. (3) Write rewrite rules for every statement form that can change the represented value; add guard assertions before using a shadow. (4) State an invariant only over the ghosts. (5) Prove the four operator conditions for every rule. (6) Apply selected rules to a source program and retain the original assertions. The paper’s square rules R1–R4 show the shape: initialization x=α sets x_sq=α² and x_shad=x; increment updates by 2α*x+α²; scaling multiplies the square; and y=x*x reads x_sq after asserting the shadow agrees (Figure 2, p. 4).

Verus form (inference). A Rust implementation would keep tracking fields or ghost variables in a verified wrapper, use requires/ensures on proof helpers, and maintain the relation with assert and invariant loop annotations. Verus has no direct schematic rewrite operator, so source rewriting or a macro would generate the ghost updates; the invariant proof remains in Verus. The shadow check is an executable assertion or a proof assertion depending on whether the shadow is ghost-only. This is an inference because the paper’s language is a core imperative language and CHCs, not Verus.

Evidence and limits. The paper reports machine-checked proofs of the square, universal, maximum, and sum operators in Frama-C, adapted to C native arrays (section 4.2, p. 16). Soundness does not make every instrumentation complete: a wrong choice may fail, and the search is only useful when some correct instrumentation exists. Operators assume the rewrite rules cover all relevant writes; a missed write triggers a guard only when the tracked interval or shadow is subsequently used.

technique 2: counterexample-guided instrumentation search

What it is. Because an operator leaves statement choices nondeterministic, the paper searches the finite space of candidate rewritings. Algorithm 1 starts with a candidate instrumentation, asks a verifier whether the instrumented program is correct, and refines the candidate set using counterexamples. For each failing candidate, it removes candidates that make the same rewrite decisions on the statements occurring in the counterexample, then tries another candidate. A successful candidate proves the original program by operator soundness. The paper says: “We propose a counterexample-guided algorithm for this purpose, which starts from some arbitrarily chosen instrumentation, checks whether the instrumented program can be verified, and otherwise attempts to fix the instrumentation using a refinement loop.” (section 1, p. 4).

Steps. (1) Enumerate or represent the candidate rewrite choices. (2) Instrument the program with one candidate. (3) Invoke the assertion verifier. (4) If it proves all assertions, stop. (5) If the counterexample ends in an original assertion, report the source program incorrect. (6) Otherwise collect the instrumented statements appearing in the counterexample and remove candidates that agree on those choices but are also incorrect. (7) Repeat until a proof, a source counterexample, or no candidates remains. Candidate verification may time out; the implementation may retry it, so attempted steps can exceed the nominal search-space size (section 5.2, p. 18).

Verus form (inference). The verifier call can be a Verus compilation/proof run over generated Rust variants. A generator can toggle ghost updates at candidate program points; failed proof traces or diagnostics provide refinement clues, although Verus does not expose the paper’s CHC counterexample format directly. assert statements corresponding to original postconditions must be distinguished from instrumentation guards before classifying a counterexample.

Evidence. MonoCera implements this strategy over constrained Horn clauses by extending Eldarica and TriCera; the same CHC encoding is usable by JayHorn, Korn, RustHorn, SeaHorn, and TriCera (section 5.1, p. 17). The algorithm’s guarantee is conditional: if a correct candidate exists and the backend eventually answers, it will not incorrectly return Incorrect; timeouts and an incomplete candidate space remain practical failure modes.

technique 3: interval tracking for universal array quantification

What it is. Operator Ω∀,P tracks a contiguous interval of an array on which predicate P holds universally. Ghosts qu_lo, qu_hi, qu_ar, and Boolean qu_P represent the interval, array snapshot, and truth value. On a store, the operator resets tracking when the write is outside or can invalidate a sole false element; otherwise it extends the interval and conjoins the new predicate value. A quantified expression checks that its range lies inside the tracked interval when qu_P is true, or contains the tracked interval when qu_P is false, then returns qu_P (Figure 4, p. 13). The invariant is qu_lo=qu_hi or qu_P = forall(qu_ar,qu_lo,qu_hi, P).

Steps. (1) Initialize an empty interval and qu_P=true. (2) Rewrite each store(a,i,x); if the interval is empty, disjoint, or the write may overwrite the only false point, reset to [i,i+1) with value P(x,i). (3) Otherwise assert the ghost snapshot equals the old array, update qu_P with P(x,i), and extend the interval for an adjacent write. (4) Rewrite select similarly, without resetting for reads inside the interval. (5) Rewrite b=forall(a,l,u,P); return true for an empty range, else assert the range relation and assign b=qu_P. (6) Prove invariant preservation for each rule. The paper explains: “If qu_P is true, then it is sufficient that quantification occurs over a sub-interval of the tracked interval, and vice versa if qu_P is false.” (section 4.1, p. 13).

Verus form (inference). Represent the interval bounds and snapshot as ghost state, use a sequence or map model of the array, and prove a quantified predicate over the interval with forall specifications. A loop invariant can maintain the interval relation; stores need lemmas for snapshot equality and range extension. Verus’s specification quantifiers differ from the paper’s forall expression, so the generated ghost proof is an adaptation.

Evidence and limits. The authors prove Ω∀,P is an instrumentation operator (Lemma 2, section 4.1). It handles contiguous ranges and may need multiple operators for disjoint access patterns. It assumes normalized quantified assignments and relies on guard assertions to reject stale snapshots.

technique 4: cancellative aggregation tracking

The aggregation framework models a finite array slice with a monoid homomorphism. Maximum uses the monoid over extended integers with max; sum uses (Z,+,0). For Ωsum, ghosts ag_lo, ag_hi, ag_sum, and ag_ar track a slice and its sum. A store outside or far from the interval resets tracking. A store inside subtracts the old value from ag_sum before adding the new value; adjacent stores extend bounds. A sum expression asserts exact array and bound equality, then returns ag_sum (Figure 5, p. 16). The paper states: “Since ∑ is cancellative, when storing inside of the tracked interval, the previous value at the index being written to is first subtracted from the sum, before adding the new value, ensuring that the correct aggregate value is computed.” (section 4.2, p. 16).

Steps. (1) Choose a monoid and homomorphism for the aggregation. (2) Initialize an empty interval. (3) Rewrite stores with reset, subtract-old/add-new, or adjacent-extension branches. (4) Update the array snapshot. (5) Rewrite aggregate reads with exact range and snapshot assertions. (6) Prove ag_lo=ag_hi or ag_sum=sum(ag_ar,ag_lo,ag_hi). Maximum additionally tracks an index of a maximum so that in-range stores do not always require a reset (section 4.2, pp. 14–16).

Verus form (inference). A Seq<int> ghost model and a spec fn sum can express the homomorphism; proof lemmas establish replacement as old_sum - old_value + new_value. Loop invariants maintain bounds and snapshot equality. Maximum needs a ghost index and a lemma connecting it to the slice maximum. These are inferred mappings; the paper verifies C/CHC operators, not Rust.

Evidence and limits. MonoCera evaluated 117 SV-COMP programs plus 26 crafted programs, with 300-second timeouts on an AMD Opteron 2220 SE at 2.8 GHz and 6 GB RAM (section 5.2, p. 18). Table 3 reports 96 forall tests, of which MonoCera verified 30; it verified 16/26 sum, 8/12 max, and 9/17 min tests. For the SV-COMP subset, MonoCera verified 42 programs, while CPAchecker verified 1 and SeaHorn and TriCera 0; on crafted arrays of size 100 or unbounded, only MonoCera succeeded (section 5.2, p. 18). The denominator is the number of tests in each operator row, not all 143 programs. The table’s “Inst. space” is candidate count and “Inst. steps” attempted candidates; retries after timeouts can make steps exceed space.

trust, reuse, and product implications

The proved object is the instrumentation operator’s preservation and soundness conditions, plus backend verification of each instrumented program. Trusted components include the verifier, CHC translation, the Frama-C adaptation used for operator proofs, and the correctness of the rewrite implementation. The paper does not prove that a specific Rust compiler or Verus translation preserves these semantics. The framework already addresses automatic ghost instrumentation for nonlinear expressions, quantifiers, and aggregation; VL should avoid reimplementing these ideas without checking whether Verus’s sequence, map, and quantifier support can host the invariants. Inference: for agent-written verified Rust, interval and sum instrumentation could reduce proof burden, but generated rewrites introduce a serious threat if a missed mutation is not guarded or if the source-to-ghost transformation is trusted outside Verus. The operator invariant and original-assertion distinction are therefore the key safety boundary.

techniques for the catalog

• sound instrumentation operators: rewrite difficult expressions with ghost state, guards, and a proved invariant
• counterexample-guided instrumentation search: refine candidate rewrite choices using verifier counterexamples
• universal interval tracking: maintain a contiguous array range and answer forall queries with range assertions
• cancellative aggregation tracking: update sums by subtracting replaced values and adding new values Checked 2026-10-14 against the paper by a Codex agent: audit record amilon2023automatic; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15