DafnyComp

DafnyCOMP is a benchmark consisting of 300 automatically synthesized multi-function programs used to evaluate large language models on compositional specification generation in Dafny, focusing on reasoning across multiple interacting functions with data dependencies.

Papers using DafnyComp (4)

Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification2025Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny2025Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification2025