# A benchmark for C program verification

## TL;DR

This paper introduces a benchmark comprising twenty-five C programs designed to evaluate and compare the effectiveness of formal verification tools, facilitating system demonstration, effort comparison, and competitive evaluation.

## Contribution

It provides a standardized benchmark with a scoring formula for assessing C program verification systems, promoting fair comparison and progress in the field.

## Key findings

- Benchmark enables systematic evaluation of verification tools.
- Scoring formula allows quantifiable comparison.
- Facilitates demonstration and competition in C verification.

## Abstract

We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last purpose, we give a scoring formula that allows a verification system to score up to a hundred points.