4 papers
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…