Showing cs.PLShow all
2 papers · 1 filter
cs.PL2025
VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
Lingfei Zeng, Fengdi Che, Xuhan Huang +4
Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specificatio…
cs.PL2025
Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification
Xu Xu, Xin Li, Xingwei Qu +2
We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-fun…