Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Verification to Herding: Exploiting Software's Sparsity of Influence

Tim Menzies, Kishan Kumar Ganguly

TL;DR

This work proposes a shift from verification and modeling to herding: treating testing as a model-free search task that steers systems toward target goals, and introduces EZR (Efficient Zero-knowledge Ranker), a stochastic learner that finds controllers directly.

Abstract

Software verification is now costly, taking over half the project effort while failing on modern complex systems. We hence propose a shift from verification and modeling to herding: treating testing as a model-free search task that steers systems toward target goals. This exploits the "Sparsity of Influence" -the fact that, often, large software state spaces are ruled by just a few variables, We introduce EZR (Efficient Zero-knowledge Ranker), a stochastic learner that finds these controllers directly. Across dozens of tasks, EZR achieved 90% of peak results with only 32 samples, replacing heavy solvers with light sampling.

From Verification to Herding: Exploiting Software's Sparsity of Influence

TL;DR

This work proposes a shift from verification and modeling to herding: treating testing as a model-free search task that steers systems toward target goals, and introduces EZR (Efficient Zero-knowledge Ranker), a stochastic learner that finds controllers directly.

Abstract

Software verification is now costly, taking over half the project effort while failing on modern complex systems. We hence propose a shift from verification and modeling to herding: treating testing as a model-free search task that steers systems toward target goals. This exploits the "Sparsity of Influence" -the fact that, often, large software state spaces are ruled by just a few variables, We introduce EZR (Efficient Zero-knowledge Ranker), a stochastic learner that finds these controllers directly. Across dozens of tasks, EZR achieved 90% of peak results with only 32 samples, replacing heavy solvers with light sampling.
Paper Structure (20 sections, 3 equations, 1 figure, 3 tables)

This paper contains 20 sections, 3 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. The Modeling Trap
  3. The Cost of $T$ (The Theory)
  4. The "Data-First" Alternative
  5. An Abductive Model of Testing (and Other Things)
  6. Evidence for Sparsity
  7. Layer 1: Logic and SAT
  8. Layer 2: Source Code Structure
  9. Layer 3: Runtime Behavior
  10. Layer 4: Requirements and Design
  11. Methodology: The EZR Recipe
  12. Formalism: Herding vs. Verification
  13. The EZR Algorithm
  14. Experiments
  15. Experimental Setup
  16. ...and 5 more sections

Figures (1)

  • Figure 1: EZR versus SMAC and other algorithms. Experiments on the MOOT data Menzies2025MOOT. Statistical analysis of 20 runs with different random seeds with scores generated by Equation \ref{['tab:results']}. Results ranked using nonparametric effect size (Cliff's Delta) and significance tests (KS-test, 95% confidence). The $y$-axis shows how often one optimizer was statistically as good as, or better than, all other algorithms (so larger y=values are better). All plots rise to a high value on the right-hand-side since, given enough samples, the performances of different algorithms mostly tie. Note that EZR (the green line) performs as well or better than SMAC (and everything else). From datalite.