MshBench: A Cross-Language Dataset for Evaluating LLM-Generated Separation Logic Specifications

MshBench is a cross-language dataset for evaluating LLM-generated separation logic specifications with VeriFast. It contains 148 tasks across C (39), Java (60), and Rust (49). Each task provides a program with reference annotations, a specification-free input, extracted reference specifications, and task metadata. This release also includes language-specific prompts, LLM-generated specification candidates, VeriFast verification logs, bounded repair traces, result tables, and scripts used to construct and analyze the dataset. Task IDs link the benchmark files to the experimental results. The README describes the directory structure, task format, and reproduction steps.