neurips2026-crychic/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.… See the full description on the dataset page: https://huggingface.co/datasets/neurips2026-crychic/crychic-dafny-acsl.