5 papers
ProofPulse: Interactive Proof Coverage Analysis for Dafny
Álvaro F. Silva, Ruben Martins, Alexandra Mendes
Deductive verification ensures that an implementation satisfies its specification, but successful verification does not guarantee the quality of the specification. As such, weak sp…
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…
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…
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…
Leveraging Large Language Models to Boost Dafny's Developers Productivity
Álvaro Silva, Alexandra Mendes, João F. Ferreira
This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as…