A benchmark for C program verification
Programming Languages
2019-04-03 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1904.01009,
title = {A benchmark for C program verification},
author = {Marko van Eekelen and Daniil Frumin and Herman Geuvers and Léon Gondelman and Robbert Krebbers and Marc Schoolderman and Sjaak Smetsers and Freek Verbeek and Benoît Viguier and Freek Wiedijk},
journal= {arXiv preprint arXiv:1904.01009},
year = {2019}
}