6 papers
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…
MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
Isabel Amaral, Alexandra Mendes, José Campos
In verification-aware languages, such as Dafny, despite their critical role, specifications are as prone to error as implementations. Flaws in specifications can result in formally…
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…
Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs
Valentina Wu, Alexandra Mendes, Alexandre Abreu
Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identif…
What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
Francisco Oliveira, Alexandra Mendes, Carolina Carreira
Software reliability is critical in ensuring that the digital systems we depend on function correctly. In software development, increasing software reliability often involves testi…
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…