Algorithm Selection for Software Verification using Graph Neural Networks

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

problem and result

The paper studies how to choose a verifier for a program and property when no verifier dominates. Its selector, Graves, turns a C program into a graph, encodes that graph with a graph neural network (GNN), and scores a portfolio of verifiers. The abstract reports evaluation on 10 tools and over 8,000 verification problems, with a 12% improvement over prior selection and 9% more problems verified than any single verifier (Abstract, p. 1). This is a portfolio-selection technique, not a new proof calculus.

technique 1: semantic program graph construction

What it is. Graves represents a program graph G=(V,E,H): AST nodes V, one-hot node encodings H, and typed directed edge sets E (§3.1, pp. 8–9). The edge sets are AST structure, interprocedural control flow graph (ICFG) control/call/return edges, and data-flow reaching-definition edges. AST nodes preserve operations, variables, and functions while discarding purely structural punctuation. ICFG edges expose paths and loops; data edges expose definitions reaching uses. The paper explains the purpose precisely: “Control flow information is vital to most, if not all, verification properties.” (§3.1, p. 8).

When to use it. Use this representation when verifier performance depends on interactions among statements, control paths, and data dependencies. A bag of counts cannot distinguish the paper’s two programs that contain the same statements but place an increment inside versus after a loop (§1, pp. 2–3). The graph preserves the difference and gives a selector a chance to learn that bounded model checking may suit one program while proving nontermination is needed for the other.

How to apply it. (1) Parse source with a compiler AST. (2) Create one node per AST token and map tokens seen in training to one-hot indices; reserve a final unknown-token index for prediction-time tokens. (3) Build an ICFG connecting statement control flow and function call/return edges. (4) Run a work-list reaching-definition algorithm to add directed data-flow edges. (5) Store the three edge sets separately so the neural layer can process their direction and type (§3.1, pp. 8–9; §3.5, p. 12). The authors’ implementation uses Clang, C++, Python, PyTorch, and PyTorch Geometric (§3.5, p. 12).

Verus form. Inference: build a Rust/Verus intermediate representation with syntax, control-flow, call/return, and borrow/data-dependence edges. Include the verification property as a graph input, because Graves appends a property-class code (reach safety, memory safety, overflow, or termination) to the graph vector (§3.3, p. 11). This is an orchestration layer around Verus; it does not change Rust contracts or Verus proof syntax. A Verus-specific graph must represent requires, ensures, invariant, assert, assume, and proof calls explicitly, because the C AST tokens used in the paper cannot encode those constructs directly.

Evidence and limits. The graph builder was checked with assertions ensuring edges reference existing AST nodes, every problem has a property and label, and graphs contain no AST cycles (§6.4.1, p. 23). The dataset is C only; the authors explicitly state that transfer to different languages or ASTs is unknown (§6.4.2, p. 23). Inference: the graph design is plausible for routing Verus jobs, but a model trained on C cannot be assumed to select a good Verus proof strategy.

technique 2: adaptive GNN selector

What it is. Graves has efficient graph convolution (EGC) message-passing layers, a jumping-knowledge layer, and a pooling layer (§3.2, pp. 9–11). EGC messages are formed from the sending node state and aggregated with several commutative functions (max, mean, and standard deviation in the best configuration). Unlike a fixed graph kernel, the learned coefficients adapt node representations to the program. Jumping knowledge concatenates intermediate and final node states so both local statements and long-range compositions can influence the result. Max, mean, and attention pools then produce a fixed-size graph vector. A three-layer fully connected network maps that vector plus the property-class integer to one score per verifier (§3.2–3.4, pp. 9–11). The paper summarizes the task as: “Given a program P and a specification ϕ, formal verification seeks to determine whether the executable program behavior is consistent with the specification, P |= ϕ.” (§1, p. 1).

How to apply it. (1) Select edge types and EGC hyperparameters; the reported best model uses AST, ICFG, and data edges, two EGC layers, aggregation {max, mean, std}, and max/mean/attention global pooling (§5.4, p. 16). (2) Run EGC message passing for each layer, concatenating each layer’s node state through jumping knowledge. (3) Apply the three pools and concatenate their outputs. (4) Append the integer property-class representation. (5) Feed the vector to the prediction network and rank verifiers by score, prioritizing correctness and then speed (§3.4, p. 11). (6) Train with pairwise margin-ranking loss on labels equal to each verifier’s SV-Comp score minus a time penalty; use batch size 5, learning rate 10^-3, 25 epochs, and reduce learning rate after three validation epochs without improvement (§5.4, p. 16).

Verus form. Inference: replace the C graph front end with Verus IR and define the portfolio as proof modes (for example, different solver configurations, lemma libraries, or bounded versus invariant-oriented workflows). The selector should rank complete proof attempts, not silently weaken contracts. Verus itself supplies no GNN layer; the model would run before invoking cargo verus, and its output would choose a configuration or proof plan. The model’s recommendation remains heuristic: each chosen proof must still pass Verus’s normal ensures and invariant obligations.

Evidence. On the 2018 SV-Comp C dataset, 9,523 problems were reduced to 8,330 for training because 13% produced graphs too large for 16 GB GPUs; the average retained graph was 8.75 MB (§5.3, p. 15). The authors use a random 80/10/10 train/validation/test split and obey SV-Comp’s 20% training limit. For successful-selection accuracy, they evaluate 680 test examples (81.8% of the test set) after removing unsolvable and universally solvable instances (§5.3, §5.6.1, pp. 15–17). Graves scores 0.856 ± 0.007 success and 0.734 ± 0.001 Spearman correlation, versus CST 0.577 ± 0.000 and 0.257 ± 0.000, and a static selector 0.697 ± 0.000 and 0.243 ± 0.000 (Fig. 5, p. 18). The paper reports a 12% (8 percentage point) Spearman improvement over WLJ (§6.1, p. 19).

technique 3: property-aware selection and operational scheduling

The same program can need different tools for termination, memory safety, overflow, or reach safety. Graves maps each property class to an integer and appends it to the pooled graph vector (§3.3, p. 11). This prevents a selector from returning one ranking for a program when the specification changes. The paper’s practical metric is Top-K error: a selector is correct when the best verifier is among its first K predictions (§5.6.3, pp. 17–18). Running the first K predictions in parallel trades resources for time. Graves places the best verifier among its first four on 87% of test problems and can verify 9.3% more problems than the best single verifier in equal time (§6.1–6.2, pp. 19–22). On the 833 test problems, 106 are unsolvable by every portfolio tool; with a 900 s limit Graves solves 76%, while a virtual best selector solves 87% (§6.2, p. 21). Its mean prediction overhead is 1 s (0.3 s best, 25 s worst), averaging 46% of total time (§6.2, p. 22).

Verus form. Inference: use Top-K as a scheduler for multiple Verus proof configurations, with a resource cap and an explicit policy for accepting the first verified result. Keep the solver result and proof artifacts so that a fast but fragile configuration can be compared with a slower robust one. The paper does not measure proof maintenance, compiler changes, or Rust ownership obligations, so those are open engineering questions for VL.

technique 4: GNN explanation for verifier-relevant features

The authors use GNNExplainer to assign each graph edge an importance score, retain the ten highest-scoring edges for each selected program, and open-code those edges into categories (§7, pp. 24–27). They inspect 40 programs (10 per technique) with fewer than 500 nodes. The 400 selected edges yield 434 code uses grouped into assertion satisfiability, non-loop branching, error reachability, small loops, large loops, and miscellaneous (Table 3, p. 26). For BMC+K, 75% of loop-related codes concern large bounds; for BMC, 85% of small-loop codes concern loop-condition variables or iterators (§7.2.2–7.2.3, pp. 27–28). The paper states: “For each algorithm, Graves’ model identifies portions of the program that an expert would use to predict the given algorithm’s success.” (Conclusion, p. 29).

Verus form. Inference: explanation can expose which contracts, loop invariants, quantified facts, or data dependencies caused a solver configuration to be selected. It can support an agent’s choice of proof tactics, but an explanation is not a proof and should never be treated as evidence that a contract is correct.

ablations, trust, and limits

Removing EGC layers reduces prediction by about 1–4%; jumping knowledge improves most counterparts by about 1%. Max pooling is the strongest single pool; all three pools give the best success and Top-K results for K<6 (Figs. 7–8, pp. 22–23). The study’s threats include researcher coding bias, C-only data, unrealistic small SV-Comp examples, and unknown transfer to other compilers and languages (§6.4, §7.3, pp. 23, 28). The model trusts labels derived from SV-Comp scores, benchmark split assumptions, compiler parsing, GNN training, and the portfolio’s verifier implementations. It does not prove a program property; each selected verifier still must establish it.

Inference: threat to agent-written verified Rust is moderate. A selector can reduce wasted proof attempts, but a distribution shift in Rust libraries or Verus specifications can make rankings wrong. VL should log the selected configuration, actual verification outcome, and timing, and retrain only from independently checked results. Existing work already covers feature-vector, AST, WLJ, CST, and GNN portfolio selection; VL should not claim the general idea as new.

techniques for the catalog

• semantic program graphs — combine AST, control/call, and data-flow edges so selection sees verification-relevant interactions
• adaptive EGC GNN — message-pass over typed edges, retain intermediate states, pool them, and score a verifier portfolio
• property-aware ranking — append the specification class so the same program can receive different verifier rankings
• Top-K scheduling — run the first K predicted verifiers under a resource limit to trade parallelism against wasted work
• GNNExplainer coding — inspect the highest-scoring edges and categorize patterns associated with each verification algorithm Checked 2026-10-14 against the paper by a Codex agent: audit record leeson2022graves; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15