Chc Comp21 Lia Lin Eval

chc-comp21-lia-lin-eval

Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification — Somorjai et al. (2024) (arXiv:2404.15215, 2024)

What this evaluates

Evaluates the effectiveness of bottom-up versus top-down transformations for solving linear constrained Horn clauses (CHCs) using software verification workflows. It measures how many verification tasks a solver can successfully resolve within a strict time limit.

Datasets

• CHC-COMP21 LIA-Lin track — total 585; splits: benchmark (585)

Metrics

• solved_tasks (primary) — range: [0, 585]
  • Count of benchmark tasks successfully solved (SAT/UNSAT proven) within the 300-second timeout. Tasks exceeding the timeout are counted as unsolved.

Input / output format

Input: Linear Constrained Horn Clauses (CHCs) over the background theory of linear integer arithmetic.

Output: Satisfiability verdict (SAT/UNSAT) or timeout status.

Scoring recipe

solved_count = 0
for task in dataset:
    result = solver.run(task, timeout=300)
    if result == "solved":
        solved_count += 1
return solved_count

Common pitfalls

• Timeouts are strictly capped at 300 seconds; partial progress or slow convergence does not count as solved.
• Baseline solvers (Z3, UNIHORN, ELDARICA) were run with their default configurations, which may not be optimized for this specific track.
• The evaluation only reports task counts; it does not measure proof/refutation generation or runtime distribution beyond a quantile plot.

Evidence (verbatim from paper)

The implementation was evaluated on 585 linear CHCs over the background theory of linear integer arithmetic from the LIA-Lin track of the CHC-COMP21 benchmark repository. The benchmarks were run on machines with 8 logical CPU cores and 16 GB of memory, with a timeout of 300 seconds. The results of the tool were either correct or timeout for all of the tasks.

Citation

@misc{somorjai2024bottoms,
  title={Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification},
  author={Somorjai et al. (2024)},
  year={2024},
  note={arXiv:2404.15215}
}

• arXiv: 2404.15215