3 papers
cs.SE2026
Improving Debugging in Verification-Aware Languages Through Automated Fault Localization: A Case Study in Dafny
Álvaro Silva, Isabel Amaral, João Pascoal Faria +1
Verification-aware languages, like Dafny, integrate formal specifications directly into source code to enable static correctness checks. However, when verification fails, the feedb…
cs.SE2025
Inferring multiple helper Dafny assertions with LLMs
Ãlvaro Silva, Alexandra Mendes, Ruben Martins
The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use o…
cs.SE2025
Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny
Carolina Carreira, Ãlvaro Silva, Alexandre Abreu +1
Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive progr…