fm-universe/Live-FM-Bench

Live-FM-bench是一个用于程序验证（形式规范生成）的持续更新且无污染的评估基准，包含360个C程序及其要验证的属性。该数据集可用于规范生成任务，输入为程序和要验证的属性，输出为可以通过验证器的带规范的程序。

Live-FM-bench is a continuously updated and contamination-free evaluation benchmark for program verification (a.k.a., formal specification generation), containing 360 C programs along with their properties to be verified. The dataset is applicable for specification generation tasks, where the input is a program and properties to be verified, and the output is a program with specifications that can pass the prover.