VeriFixer: Automated Repair of Verification-Aware Languages

VeriFixer aims to assist programmers in fixing code issues identified by software verifiers, a task that remains largely manual despite advancements in automatic program repair.

Verification-aware languages help ensure software correctness by detecting violations of formal specifications. While these languages aid developers in identifying flaws, repairing them still requires significant manual effort. VeriFixer seeks to bridge this gap by building an open-source tool that automates code repair in verification-aware languages, starting with Dafny, a language used by companies like Amazon Web Services.

The project was funded in the highly competitive FCT Exploratory Projects call, which had an acceptance rate of 21%. It is a collaboration between researchers from INESC TEC, INESC ID, and Carnegie Mellon University. In addition to developing repair techniques, VeriFixer will create publicly available datasets with real-world examples to drive further research in this area. By advancing automatic repair methods, VeriFixer contributes to making software development more efficient and reliable, particularly in critical domains such as healthcare, aerospace, and finance.