Domain Types Eval

domain-types-eval

Domain Types: Selecting Abstractions Based on Variable Usage — Apel et al. (2013) (arXiv:1305.6640, 2013)

What this evaluates

Evaluates the effectiveness and efficiency of software model checking configurations that use domain types to select abstract domains (BDD vs explicit-value) for variable abstraction. It probes how well different abstraction strategies handle verification tasks across various benchmark suites.

Datasets

• SV-COMP and RERS benchmark sets (SYSTEMC, ECA, LOCK, PRODUCT SIMULATOR, NTDRIVERS, SSH) — total ?; splits: test (-1)

Metrics

• Effectiveness (primary) — range: percent
  • Percentage of verification tasks correctly solved by a configuration out of the total tasks in the benchmark set.
• Efficiency — range: other
  • Accumulated CPU time in seconds across all correctly solved verification tasks, typically visualized via quantile plots where the x-axis is task rank and the y-axis is time.

Input / output format

Input: C source code programs with verification properties (e.g., safety assertions, invariants) to be checked by a model checker.

Output: Verification outcome per task: correctly solved, timeout, out-of-memory, or abstract domain limitation failure.

Scoring recipe

def compute_metrics(predictions, gold_tasks):
    total = len(gold_tasks)
    solved = sum(1 for p in predictions if p.outcome == 'correctly_solved')
    effectiveness = (solved / total) * 100
    efficiency = sum(p.cpu_time for p in predictions if p.outcome == 'correctly_solved')
    return {'effectiveness': effectiveness, 'efficiency': efficiency}

Common pitfalls

• Timeouts and out-of-memory terminations are counted as failures but do not indicate logical incorrectness.
• Combined configurations may mask the performance of individual abstract domains, making it hard to isolate which domain type caused a speedup or slowdown.
• Quantile plots aggregate performance, so individual outlier tasks can skew the perceived efficiency.

Evidence (verbatim from paper)

Effectiveness. Table II gives an overview of the number of correctly solved verification tasks. Each row shows the results for one benchmark set. For each configuration, we show which percentage of the verification tasks could be correctly solved. ... Efficiency. Before we discuss the details, we briefly give an overview over the results, based on Fig. 8. The diagrams show the performance of the configurations in separate quantile plots for each benchmark set. A point (x,y) in a quantile plot states that the x th-fastest verification run of the respective configuration took y s of CPU time.

Citation

@misc{apel2013domaintypes,
  title={Domain Types: Selecting Abstractions Based on Variable Usage},
  author={Apel et al. (2013)},
  year={2013},
  note={arXiv:1305.6640}
}

• arXiv: 1305.6640