Finding Model-Checkable Needles in Large Source Code Haystacks: Modular Bug-Finding via Static Analysis and Dynamic Invariant Discovery

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

what the paper does

The paper proposes “a novel marriage of static and dynamic analysis” (abstract, p. 1). Its goal is scalable bug finding, rather than a proof that an entire code base is correct. It searches a large code base for small functions that a model checker can handle, then mines likely input preconditions from an existing test suite. The authors call this search “verification task triage” (p. 2). The selected functions are then model checked with the mined facts as assumptions (Figure 1, p. 2); the paper’s examples use the bounded model checker CBMC (Section II, Figure 4; Section III).

The paper’s central claim is that a deliberately incomplete workflow can still find real faults. It seeks functions with assertions or evident safety properties and simple control flow, while excluding recursion, recursive data types, difficult pointer manipulation, and other features that frustrate model checkers (pp. 1–2). Dynamic invariants are propositions true on observed executions; the paper uses them as approximate preconditions to remove uninteresting counterexamples. The abstract says: “While providing little in the way of verification, this approach may provide an additional quick and highly scalable bug-finding method for programs that are usually considered “too large to model check.”” (p. 1). Inference: its demonstrated result is bug discovery on bounded models, not a sound whole-program proof.

technique: triage functions before model checking

What it is. Triage is a static filter that finds self-contained functions whose code already exposes a property to check. The prototype selects functions that contain an assertion or potentially crashing memory dereference and whose parameters and locals can be resolved to simple C types (int, short, long, void, and char) (Section III, p. 4). The paper says the filter was “automatically identified using a very simple 100-line Python script that crawls through a set of C source files and identifies functions that” satisfy these two conditions (Section III, pp. 3–4). The broader idea is to avoid functions with recursion, recursive data types and complex pointer manipulation (Introduction, p. 2), but the paper says the prototype does not filter out recursion or references to global values of “bad” types (Section III, p. 4).

When to use it. Inference: use this when a complete system is too large for model checking but a useful safety or assertion property is repeated in many functions. The authors motivate the scale problem with Curiosity rover software: model checking was applied to portions “typically 10,000 lines or less,” while the full software was approximately 2 million lines (p. 1). Triage lets a tool inspect the large code base and present many small candidates instead of asking a human to select one or two.

How to do it. Inference: the numbered steps below are this study’s reconstruction; the paper states only the two selection conditions and does not give a step list or say how types were resolved. (1) Parse each source file and enumerate functions. (2) Resolve each function’s parameter and local types; retain simple scalar and character types in the prototype. (3) Retain functions containing an assertion or an access that could crash. (4) Reject or later inspect functions that use recursion, global values of unsuitable types, complex structures, or calls whose summaries cannot be resolved. (5) Ground remaining types and choose finite bounds for model checking. The paper states that the prototype is both “over-restrictive” and “not restrictive enough” (Section III, p. 4): functions taking structures or arrays can often be handled easily, while recursion and references to global values of “bad” types are not filtered out. It expects triage to “require a deeper static analysis that includes more types and uses summaries of functions called by a function” (Section III, p. 4), and says the first steps require “a complete analysis of the accessed data types and call graphs from each function” (Section IV, p. 5).

Verus form. Inference: use a Rust/Verus wrapper that exposes a candidate’s safety contract as requires and ensures, then prove a bounded or finite abstraction with executable code separated from spec and proof code. A candidate filter can search for functions with assert, indexing, pointer wrappers, or calls with available specifications, and reject unsupported recursion or opaque external calls. Verus does not automatically turn a C assertion into a complete functional contract; the engineer must state the postcondition and any ownership or memory facts. The C prototype’s finite type grounding carries over as explicit requires bounds, but CBMC’s harness syntax and arbitrary C memory model do not.

Evidence and limits. On roughly 40K lines of non-comment SpiderMonkey 1.6 C, the script selected 11 possible verification targets (Section III, p. 4). The paper says the 11 “include some unsuitable targets (including one case where the textual type analysis fails to notice a complex compiler state structure)” and that “A few functions are simple bit-twiddling or offset-computing code that can be trivially verified without invariants.” This denominator is the 40K-line SpiderMonkey subset, not a benchmark of all code bases. The filter found a Boyer–Moore–Horspool function, which the authors call “of considerably more interest.” It is a search heuristic, and the paper reports no precision, recall, or soundness measurement for the 11-function selection.

technique: mine dynamic invariants as approximate preconditions

What it is. The workflow instruments selected code, runs the existing test suite, and gives traces to Daikon. Daikon infers “empirical” invariants: propositions that hold on all observed executions. The inferred relations are inserted as assumptions before model checking. The purpose is to carve away inputs that tests and system context suggest are impossible, reducing false positives. The paper emphasizes that the invariants need not be exact: “Our claim is that our use of dynamic invariants relies on their ability to crudely “carve away” the data values that a function is not expected to work rather than on their strict accuracy.” (Introduction, pp. 2–3).

When to use it. Inference: use this when unannotated environmental or protocol preconditions make unconstrained model checking produce many irrelevant failures. A function taking an int m might in practice receive minutes since midnight; the type system does not state that range. The paper’s example adds 0 <= m < 3600, which lets the model checker report the real bug instead of an integer-overflow counterexample from multiplying m by 60 (Introduction, p. 2). The authors also discuss a poor test suite: “if the test suite falsely suggests that 0 <= m < 60 because tests only run for 1 hour, the model checker can still find the real bug” (Introduction, p. 2). Inference: the off-by-one bug at m = 1 lies inside that under-approximated range, so this example shows tolerance of an inaccurate range, not of a range that excludes the failing input.

How to do it. Inference: the numbered steps are this study’s reconstruction from the workflow in Figure 1 and Section II. (1) Add instrumentation for branch counts, values, and other history variables; the paper calls these extended invariants (Section II, p. 3). (2) Run the available test suite or generated tests and collect traces. (3) Run Daikon over all traces. (4) Inspect the inferred ranges and relations for gross under- or over-constraints. (5) Encode them as harness assumptions or function preconditions. (6) Run the model checker on the annotated fragment and inspect counterexamples against the assumed environment. In the binary-tree example, the authors use 5,000 random tests, each with a maximum operation length of four, and infer branch-count facts such as this.br1 one of { 0, 1, 2 } and this.br3 one of { 0, 1, 2 } (Section II, p. 3). The paper says these invariants “radically underapproximate the behavior of the class.” The test generator chooses one of add, remove, and find, then asserts SUT.RepOK() after each operation (Figure 3, p. 4).

Verus form. Inference: represent mined facts as requires clauses on a verified entry point or as assume statements only at an explicitly trusted boundary. Use requires 0 <= m < 3600 for a documented environmental contract, and prove the body with loop invariants and assert facts. A trace-mined fact is evidence for choosing a contract, not a proof of the contract; placing an unreviewed assume inside verified code would make the result conditional on an untrusted premise. Daikon’s history variables have no direct executable Verus equivalent; encode the relevant relation as a ghost/spec variable and prove it from the Rust state transitions, or keep it as test-only evidence.

Evidence and limits. In the binary-tree demonstration, a shallow harness with the inferred branch bounds lets CBMC “find the bug in binary tree [8], despite the fact that the shallow random testing did not discover the bug” (Section II, p. 3); the authors chose to verify the remove function there, but the text does not say where the bug is. The paper reports no count of false positives before and after inference, no test-suite coverage percentage, and no independent validation of Daikon’s assumptions. A short random test can underapproximate behavior severely; conversely, an incorrect invariant can exclude the failing input. The result is therefore conditional bug finding, not sound verification. The paper also warns that small input bounds can create false positives when small inputs produce larger outputs (Section III, p. 4).

technique: construct a bounded harness around the selected fragment

What it is. A harness supplies symbolic inputs, invokes the candidate, asserts the target property, and constrains the state with mined facts. Figure 4 uses symbolic values v1 through v4, calls add three times, assumes branch-count ranges, calls remove, and asserts repOK. The figure comment says “Using calls for simplicity; in practice would encode structure from Daikon invariants as a series of assumptions.” (Figure 4, p. 4). The assumed counters in Figure 4 are br1 and br2, whereas the Daikon output shown in the text lists this.br1 and this.br3; the paper does not explain the difference.

How to do it. (1) Declare symbolic inputs for the operation sequence and data values. (2) Call setup operations that establish a reachable state. (3) Add assumptions for inferred ranges and structural validity. (4) Call the target operation. (5) Assert representation invariants, memory safety, or explicit assertions. (6) Choose a loop-unwinding bound justified by the triage and trace evidence. CBMC then searches the finite state space for a counterexample.

Verus form. Inference: write a proof fn or verification-only harness that calls requires-constrained functions and finishes with assert or an ensures proof; keep symbolic values in the specification layer. Verus’s proof fn is erased and cannot be called as runtime test code. A bounded harness can establish a lemma for a fixed number of operations, but a general loop requires an inductive invariant and a termination argument. CBMC’s unwinding assertion and C assume syntax do not carry over directly.

Evidence and limits. For the binary tree, the paper says the “extremely restricted harness” was enough for CBMC to find the bug despite the shallow random tests (Section II, p. 3). Inference: this demonstrates a counterexample under the harness assumptions, not correctness for arbitrary trees. For the binary tree the paper gives no unwinding completeness result and no count of explored states. Its approach can miss bugs requiring larger structures or inputs, and can report failures introduced by an unrealistic finite encoding.

technique: infer complexity and safety facts from a small model

The SpiderMonkey case applies the same workflow to js_BoyerMooreHorspool. After resolving types to ground C types and choosing string sizes based on jsfunfuzz tests, the authors increase loop bounds. They report that this both verifies memory safety for chosen strings and “discover[s]” the algorithm’s worst-case complexity where unwinding assertions held (Section III, p. 4). Introducing an off-by-one error was, in the authors’ words, detected instantly by CBMC (“CBMC instantly detects the error”), in a case they believe testing would not find. The analyzed strings are small, so the authors say it is “not a complete verification of the Boyer-Moore-Horspool implementation in SpiderMonkey” (Section III, p. 4). They also rely on an informal “small model” assumption for bug finding.

Inference: in Verus, a related experiment would specify slice bounds and a loop variant, prove memory safety for arbitrary lengths, and separately measure or prove a complexity bound using ghost counters. A bounded test can reveal a likely worst-case path but cannot establish asymptotic complexity. The paper’s evidence is one implementation and one injected error; it supplies no denominator of mutation variants or detection rate.

what is proved, measured, and trusted

The paper measures feasibility examples: 5,000 four-step random tests for the binary tree; 11 candidates from about 40K SpiderMonkey lines; a CBMC counterexample for the binary-tree remove bug; and an injected Boyer–Moore–Horspool off-by-one bug detected immediately. It does not report a systematic benchmark, false-positive rate, proof coverage, or soundness theorem. Inference: trusted components include the test suite, Daikon’s invariant inference, type and call-resolution scripts, finite bounds, harness assumptions, CBMC, and the correctness of the stated target property. Inference: a Verus product using this idea would inherit the trust problem for mined environment assumptions and external code, even if the selected Rust function body receives a machine-checked proof.

techniques for the catalog

• static verification triage — scan large code bases for small functions with assertions or safety-relevant accesses and model-checkable types
• dynamic invariant preconditions — mine test traces with Daikon and encode likely ranges and relations as harness assumptions
• bounded fragment harness — call a selected function with symbolic inputs, inferred assumptions, and an asserted property
• small-model bug finding — use finite unwinding and small inputs to expose safety faults or likely worst-case paths

Last edited: 2026-10-17