ACM SIGSOFT Distinguished Paper Award at ICSE 2025

Congratulations to Nuno Saavedra and João F. Ferreira for winning an ACM SIGSOFT Distinguished Paper Award at ICSE 2025 for their paper “Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification”.

Nuno Saavedra and João F. Ferreira, in collaboration with researchers from the University of California San Diego, Imperial College London, and the University of Massachusetts, have received the ACM SIGSOFT Distinguished Paper Award at the International Conference on Software Engineering (ICSE) 2025.

The paper “Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification,” introduces an innovative automated proof synthesis tool that uses machine learning and large language models with retrieval augmentation techniques. Rango dynamically identifies and incorporates relevant proofs and premises during each step of the verification process, adapting to both the project context and the evolving state of the proof. Tested on the researchers’ newly created CoqStoq dataset of over 2,200 open-source Coq projects, Rango successfully synthesized proofs for 32% of theorems—representing a 29% improvement over previous state-of-the-art tools and demonstrating its potential to make formal verification more accessible to developers.

The research team also includes Robert Thompson (University of California San Diego), Pedro Carrott (Imperial College London and a former MSc student at our group), Kevin Fisher (University of California San Diego), Alex Sanchez-Stern (University of Massachusetts), Yuriy Brun (University of Massachusetts), Sorin Lerner (University of California San Diego), and Emily First (University of California San Diego).

ICSE is the premier conference in software engineering, and the ACM SIGSOFT Distinguished Paper Award recognizes papers of exceptional quality presented at the conference. This achievement highlights our department’s commitment to excellence in research and international collaboration.

Congratulations to Nuno, João, and the entire research team on this outstanding achievement!