Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Survey of annotation generators for deductive verifiers

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

scope and measured baseline

This survey covers specification inference tools for deductive verification of Java programs. Its purpose is to identify what each tool infers, how much of the specification-writing workload that type could cover, and what remains unsolved. The authors distinguish main behavioral specifications from auxiliary proof annotations such as loop invariants. Their three OpenJML-verified examples are a counter, binary search, and ArrayList, requiring 32, 16, and 103 annotations respectively, 151 total; 17 avoid overflow/underflow warnings and four avoid PossiblyBadArrayAssignment warnings (Sec. 3, p. 2). The experiments use each tool’s default settings and a supplied program, tests, and sometimes Javadoc. The paper states: “Deductive verifiers require intensive user interaction in the form of writing precise specifications, thereby limiting their use in practice.” (abstract, p. 1)

The successful tool runs measured generated annotations against that 151-annotation baseline. Daikon generated 158, with 29 correct baseline annotations (19% coverage), 83 wrong (53%), and 47 correct but unnecessary (30%). EvoSpex generated 25: 8 baseline (4% coverage), 6 wrong (24%), and 11 unnecessary (44%). Strongarm generated 60: 23 baseline (15%), no wrong annotations, and 37 unnecessary (62%). ChatGPT (GPT-4) generated 42: 35 baseline (24%), six wrong (14%), and one unnecessary (2%) (Table 2, p. 12). Toradocu/Jdoctor generated none on these examples. Table 1’s average runtimes, over five runs, are tool- and example-specific: Daikon 9–28 s, EvoSpex 96 s to 4,843 s, Strongarm 2–4 s, Toradocu/Jdoctor 4–41 s; ChatGPT took about 30 s for a complete response but could not be measured as a separate process (Table 1, p. 11).

Table 2 has internal arithmetic inconsistencies: Daikon’s categories sum to 159, not its reported total of 158. EvoSpex’s 8/151 is about 5.3%, not the reported 4%; the prose’s 8/30 postconditions is about 26.7%, not 20%. GPT-4’s 35/151 is about 23.2%, not 24%. These are calculations from the printed counts, not a reconstruction of the underlying artifact. Table 1 and the Daikon prose also differ slightly on runtimes: the study uses Table 1’s values (Sec. 3.1.1, p. 4; Sec. 3.1.5, p. 6; Tables 1–2, pp. 11–12).

technique: dynamic invariant detection from executions

What it is: Daikon instruments executions, observes variables at method entry and exit, and instantiates invariants from a built-in grammar. The grammar includes equalities and inequalities, array-element relations, quantified element comparisons, divisibility, polynomial forms, null implications, membership, and substring relations (Sec. 3.1.1, pp. 3–4). The paper summarizes: “Daikon uses a dynamic approach where it observes several program executions.” (Sec. 3.1.1, p. 3)

How: (1) supply unannotated code and a test suite; (2) run the instrumented program; (3) let Daikon instantiate candidate preconditions, postconditions, invariants, and assignable/modifies clauses; (4) for a loop, add a no-op dummy_call receiving variables of interest at the loop head, then turn identical generated pre/postconditions for that dummy procedure into loop invariants (Listings 2–3, pp. 3–4); (5) manually review and retain only specifications that express intended behavior. The authors’ binary-search workaround produced a quantified sortedness relation, but the tool also inferred an incorrect claim that the list size was always zero for ArrayList’s contains method (Sec. 3.1.1, p. 5).

Verus form: Inference: instrumenting a Rust program can supply candidate observations, but Verus annotations must be written as requires, ensures, invariant, and decreases; there is no direct Daikon grammar or automatic conversion. A candidate quantified property over Seq must be proved by Verus and checked against intent. The dummy-call trick is an inference aid, not a Verus construct.

Limits and evidence: generated facts are guaranteed only for observed executions, can describe behavior rather than intent, and are limited to the grammar. The 158-annotation result contained 83 wrong facts, so output requires review (Sec. 3.1.1, p. 4).

technique: dynamic extensions and test-guided synthesis

eChicory extends Daikon by reevaluating variable structure, allowing relations that are established dynamically, such as model-view links (Sec. 3.1.2, p. 5). It retains Daikon’s grammar and test-suite dependence; the authors could not run it successfully. DynaMate combines EvoSuite-generated executions, Daikon and Gin-Dyn dynamic invariant candidates, and ESC/Java proof attempts. Gin-Dyn mutates postconditions into loop-invariant candidates, rejects candidates falsified by tests, and asks ESC/Java to prove survivors; EvoSuite generates new tests when proof fails (Sec. 3.1.3, p. 5). The survey quotes DynaMate’s published evaluation: “it automatically built correctness proofs for 23 out of 26 subjects” (Sec. 4, p. 13). This starts with supplied method contracts and measures completed subjects, rather than the fraction of all annotations generated. The survey’s authors could not run its artifact (Sec. 3.1.3, p. 5).

EvoSpex uses bounded exhaustive test generation, records valid pre/post states, mutates states to obtain invalid examples, and uses a genetic algorithm to generate a postcondition that accepts valid states and rejects invalid states (Sec. 3.1.5, p. 6). Use it for reference structures where Daikon’s simple grammar is insufficient. Its measured 25 annotations included 6 wrong and 11 unnecessary; array properties were unsupported in the tested implementation. Inference: an EvoSpex-to-Verus pipeline would need a Rust state generator, a mutation oracle, and a translator from evolved expressions to Verus syntax, followed by proof checking.

ALearner executes test cases, separates failing and successful states, learns an assertion with either predefined templates/Boolean combinations or an SVM linear inequality, then actively generates new states near the classification boundary and repeats until convergence (Sec. 3.1.7, pp. 6–7). Its active-learning overhead averaged 40 s per assertion in the cited evaluation; it remains dependent on executable behavior and can learn a wrong assertion from a wrong program. DIG/SymInfer uses symbolic execution at marked locations, then infers nonlinear equalities up to degree two, octagonal inequalities, and linear relations among (including nested) array elements; it removes violated and redundant candidates afterward (Sec. 3.1.8, p. 7). It needs a marker function carrying in-scope variables and was not runnable for Java in the survey artifact.

SLING is the shape-analysis variant: given a program location, predicate templates, and sample inputs, it captures heap traces, iteratively grows separation-logic predicates for each pointer until explored regions are described, and presents the resulting assertion (Sec. 3.1.6, pp. 6–7). It can infer heap shape but not permissions, concurrency, disjunctions, or numeric relations; reported inference times ranged from 10 s to over 14 min in its cited evaluation. Inference: for Verus, use a View/ownership model and explicit lemmas for shape and disjointness; SLING’s separation-logic predicates do not transfer syntactically.

technique: static candidate generation and proof filtering

Houdini generates heuristic candidate annotations for an unannotated program and uses ESC/Java to prove each; unprovable candidates are discarded. It can infer preconditions, postconditions, and invariants, including library assumptions when source is unavailable (Sec. 3.2.1, p. 7). Its pessimistic library assumptions cause false alarms, while optimistic non-null assumptions can miss errors. The cited Cobalt run took 62 hours for 36,000 lines, so inference cost can be substantial.

Strongarm computes a strongest postcondition from a supplied precondition (default true), simplifies duplicate and tautological clauses, and emits compact behavior clauses, preconditions, postconditions, and assignable clauses (Sec. 3.2.2, pp. 7–8). It distinguishes branches from if statements and supports \old, \result, and array .length, but not exceptional postconditions or quantified postconditions in the experiments. Its 60 generated clauses had 23 necessary baseline clauses and no wrong clauses, but 37 were unnecessary.

The KeY projects use symbolic execution plus predicate abstraction to infer loop or recursive-call specifications. A later data-dependence approach symbolically executes the loop body assuming a candidate, checks whether it still holds, and combines failed candidates with post-state information until a fixpoint (Sec. 3.2.3, p. 8). These candidates reflect actual code behavior, including bugs. Inference: Verus can express the resulting loop facts with invariant and prove a decreases measure, but the inference algorithm and abstract domains would have to be implemented separately.

techniques: user-selected observations and API usage mining

Agitator combines generated test inputs with dynamic invariant detection, shows observations in Eclipse, and lets the user choose which become assertions. This makes intent review part of the workflow, although conversion to contracts needs further work. The survey reports that Agitator’s original evaluation found 11% of observations useful; no publicly available artifact was found (Sec. 3.1.4, p. 5).

The API-precondition mining project analyzes many client programs using the same API. Build each caller’s control-flow graph, identify conditions controlling the API call, normalize equivalent conditions, infer selected implicit conditions, remove singleton or rarely checked conditions, and rank the remaining receiver, argument and combined conditions. This depends on frequent usage reflecting correct API requirements; repeated misuse can instead become a reported condition. The authors found no public artifact (Sec. 3.2.4, pp. 8–9).

The related-work section adds permission inference with Sample and Sip4J, shape and predicate inference, automatic predicate opening/closing and lemma application, and Horn-clause contract inference. Sample generates Viper array permissions; Sip4J’s Plural permissions are not immediately usable in general deductive verifiers (Secs. 6.3–6.5, p. 15). It also describes AIMS, which selects useful mutants to reduce inference work, and DeltaSpec, which generates specifications describing changes between commits (Sec. 6.6, p. 15). These are surveyed techniques, not results reproduced on the three examples.

technique: natural-language-to-specification translation and LLM generation

Toradocu/Jdoctor extracts Javadoc conditions and maps natural-language subjects and predicates to Java expressions using lexical matching (Levenshtein distance) and semantic matching (Word Mover’s Distance), then emits normal and exceptional pre/postconditions (Sec. 3.3.1, pp. 9–10). Ambiguous wording and naming mismatches can produce wrong mappings; the tested run generated no usable annotations. C2S extracts words from comments, looks up word-token pairs learned from JDK documentation and JML, assembles grammar-constrained candidates, converts them to assertions, and filters candidates against developer tests (Sec. 3.3.2, pp. 9–10). It handles void methods and exceptional behavior but cannot express existential quantifiers in its grammar and can encode observed behavior instead of intent.

ChatGPT accepts code and a prompt and can output many annotation kinds without a fixed template. The survey used three modes: generate from code, translate documentation, and generate from deliberately renamed or incorrect code (Sec. 3.3.3, pp. 10–11). GPT-4 produced 42 annotations, 35 of which matched baseline (83% of its output and 24% of the baseline), six wrong, and one unnecessary (Table 2, p. 12). It generated a quantified ArrayList removal postcondition, but also invented an undocumented precondition and produced a logically weak remove condition. Renaming methods and changing an implementation changed its output; ChatGPT also modified or renamed code, and repeated instructions to preserve it eventually yielded uninformative true contracts for some methods (Sec. 3.3.3, p. 11); GPT-3.5 misplaced annotations and produced simpler specifications. The authors rank ChatGPT first on these examples and report 24% baseline overlap (Sec. 3.4, p. 11); the printed counts imply about 23.2%.

Verus form: Inference: an LLM can draft Rust requires, ensures, invariant, decreases, spec fn, and proof blocks, but every draft must compile and pass Verus; prompt output is not evidence. Include the requested specification kinds explicitly, preserve the implementation, and check old-state expressions with Verus old(...). The survey’s GPT-4 numbers are Java-only and cannot establish Verus success.

impact, gaps, and ideal workflow

The survey maps inferred types onto a taxonomy built from 54 randomly chosen verified examples and 95% t-intervals. Behavioral specifications account for 47–62% of required annotations; proof assistance 9–22%, permissions 9–17%, and functions 5–15% (Sec. 4, p. 12). The authors estimate maximum impact by selecting taxonomy categories that encompass each tool’s output and summing their interval endpoints: Daikon/eChicory 41–77%, EvoSpex 14–23%, Strongarm 16–31%, SLING/Houdini 37–64%, and ChatGPT 0–100% because the prompt can request any type (Table 3, p. 13). Inference: intervals derived from category frequencies across sampled programs are workload estimates, not universal mathematical upper bounds for every program. The authors also caution that the three evaluation programs are not representative of all possible verified programs (Sec. 4, p. 12).

The paper’s ideal generator should output multiple specification languages; cover behavioral, permission, and proof-assistance types at method, class, and loop locations; insert annotations automatically; require no source changes, hints, or manual rewriting; target intent rather than behavior; select among inference techniques; and produce mostly correct, useful, readable annotations (Sec. 5, pp. 13–14). The research challenges in Sec. 7 (p. 16) are inference of permissions, predicates, lemmas and other proof assistance; additional truth sources such as documentation, usage, similar programs, and user answers; and generators for non-Java verifiers. The survey notes that Rust’s type system can encode some memory-safety permissions automatically, reducing specification burden, but functional behavior still needs explicit contracts (Sec. 6.8, p. 16).

Inference: for VL, these results imply that automated annotation drafting can reduce repetitive contract work but cannot be trusted without independent Verus checking and intent review. The largest threat is plausible but wrong behavior specifications, especially when code or tests are incomplete; the catalog should therefore treat dynamic and LLM outputs as candidates, not proofs. What the paper has already done is a broad taxonomy and three-example comparison; VL should not redo that as a claim of novelty. A useful remaining experiment is a Verus benchmark with denominator-reported coverage of contracts, loop invariants, permissions/ownership facts, proof lemmas, compile success, proof success, wrong-but-provable specifications, and repair time.

techniques for the catalog

  • dynamic grammar mining — observe executions and instantiate candidate contracts, invariants, and frame clauses
  • loop-invariant workaround — pass loop variables to a dummy procedure and convert matching pre/postconditions into invariants
  • test-and-proof iteration — mutate or generate tests, reject candidates by counterexamples, and retain only proof-compatible facts
  • genetic postcondition synthesis — evolve expressions that accept valid and reject invalid pre/post states
  • active-learning assertions — classify observed states and generate new states near the candidate boundary
  • symbolic nonlinear inference — solve polynomial, inequality, and array-relational candidates from symbolic/concrete states
  • shape inference — iteratively construct separation-logic heap predicates from traces and templates
  • Houdini filtering — generate heuristic candidates and discard those the verifier cannot prove
  • strongest-postcondition inference — compute and simplify branch-sensitive postconditions from a precondition
  • natural-language translation — map documentation words to code expressions and filter grammar candidates with tests
  • LLM annotation drafting — prompt a language model for requested specification kinds, then compile and verify every result
  • user-selected observations — let developers turn observed properties into assertions after reviewing intent
  • API usage mining — normalize and rank frequent conditions at client call sites
  • taxonomy impact estimation — map inferred specification types to empirical category intervals to estimate potential workload coverage

Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “These 95% confidence intervals was calculated as follows: given a set of 54 randomly chosen verified examples, the specifications were categorized according to the taxonomy (Lathouwers and Huisman, 2022).”): read the full 24-page paper text including both appendices, references and author biographies, and the whole study; checked quotes, counts, percentages, tool steps, source locations and study limits; corrected tag, page/section errors and unsupported examples, recorded inconsistent printed arithmetic, clarified impact estimates, and added omitted techniques; did not run tools or the artifact, audit annotation classifications, verify cited evaluations independently, or visually inspect the PDF.

Last edited: