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 component boundaries.

Papers using DafnyCOMP (3)

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 Dafny2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification2025