acsl
Datasets
All datasets matching “acsl”crychic-dafny-acsl
CRYCHIC Dafny-to-ACSL-C Verified Translation Benchmark
This anonymized review artifact accompanies the NeurIPS 2026 Evaluations and Datasets submission:
CRYCHIC: A Universal Framework for Cross-Language Verified Code Translation.
CRYCHIC translates verified Dafny programs into C programs annotated with ACSL specifications, then checks the generated artifacts with Frama-C WP. This release contains the 1,679 fully verified Dafny/C+ACSL pairs used as the positive benchmark corpus.
The… See the full description on the dataset page: https://huggingface.co/datasets/neurips2026-crychic/crychic-dafny-acsl.AcslBench
AcslBench: A Verified C/ACSL Dataset with Compositional Call Chains
📌 Overview
AcslBench is a large-scale verified dataset designed for formal C specification synthesis. It addresses the "data drought" in the C/ACSL domain by distilling over 500,000 verified instances from the Rust/Verus ecosystem.
The core contribution is the introduction of Compositional Call Chains, providing a high-fidelity "gold standard" for evaluating the logical reasoning capabilities of Large… See the full description on the dataset page: https://huggingface.co/datasets/noBuggie/AcslBench.ACSLBench
ACSLBench
ACSLBench is a benchmark dataset for natural-language-to-ACSL specification generation and C program verification. Each task contains a natural language requirement, a corresponding ACSL function contract, and an ACSL-annotated C program that can be used for formal verification experiments with Frama-C.
The dataset is designed for research on large language models, program specification generation, formal methods, and safety-critical C software verification.… See the full description on the dataset page: https://huggingface.co/datasets/yzrsdad/ACSLBench.CRYCHIC-Dafny-ACSL