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 checked with CBMC or a similar bounded model checker after the mined facts are encoded as assumptions.

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 authors explicitly say that the method “providing little in the way of verification” (abstract, p. 1). Thus its measured 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). It avoids functions with hard-to-model control flow and data types. The paper says the filter was implemented as “a very simple 100-line Python script that crawls through a set of C source files and identifies functions that” satisfy these conditions (Section III, p. 4).

When to use it. 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. (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): arrays and structures can sometimes be handled, while recursion and bad globals can slip through. Future work therefore requires deeper type, call-graph, and model-checker-specific analyses (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). Some were unsuitable because type analysis missed a compiler-state structure; some were trivial bit-twiddling functions. 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 considered a useful target. 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” (Section II, p. 3).

When to use it. 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 prevents an overflow counterexample caused solely by an enormous unconstrained m while retaining an off-by-one bug at m = 1 (Section II, p. 2). The authors also discuss a deliberately bad test suite: if tests suggest 0 <= m < 60, a real bug can still be found outside that observed range.

How to do it. (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, pp. 2–3). The test generator chooses one of add, remove, and find, then asserts SUT.RepOK() after each operation (Figure 3, p. 3).

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 a known remove bug that the random tests did not expose (Section II, p. 3). 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 comments that production use would encode the Daikon invariants “as a series of assumptions” rather than make calls merely for simplicity (Section II, p. 3).

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 harness’s restricted bounds are enough for CBMC to expose the remove fault despite four-step random tests. This demonstrates a counterexample under the harness assumptions, not correctness for arbitrary trees. 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). Injecting an off-by-one error produced an immediate CBMC finding. The analyzed strings are small, so the authors explicitly say this is not complete verification of the implementation.

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. 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.

Inference: the method threatens a verified-Rust product mainly through false confidence in inferred preconditions. It can help prioritize functions and discover missing contracts, but an agent must turn each useful invariant into a reviewed requirement and then prove it from the actual Rust API or system model. Existing work already supplies dynamic invariant detection, bounded model checking, and modular/assume-guarantee reasoning; VL should not present this paper’s triage-plus-mining combination as a new general verifier without measuring its precision and assumption failures.

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 Checked 2026-10-15 against paper alipour2016finding: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15