fm-universe/FM-bench-verified

FM-Bench-Verified数据集是一个包含280个C程序、待验证属性以及相应ACSL规格的手动清理和验证过的基准。该数据集可用于规格生成任务，支持输入程序和待验证属性，输出能够通过验证器的带规格程序。数据集来源于FM-bench、AutoSpec以及多个GitHub仓库，所有案例均可以通过Frama-C的WP验证。

The FM-Bench-Verified dataset is a manually cleaned and verified benchmark containing 280 C programs, properties under verification, and corresponding ACSL specifications. It can be used for specification generation tasks, taking programs and properties to be verified as input and outputting programs with specifications that can pass the prover. The dataset originates from FM-bench, AutoSpec, and multiple GitHub repositories, with all cases verifiable through Frama-Cs WP.