ACM SIGSOFT Distinguished Paper Award at ICSE 2025

Our paper “Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification” has received an ACM SIGSOFT Distinguished Paper Award at ICSE 2025.

The paper 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.

This is a collaboration with Robert Thompson (University of California San Diego), Nuno Saavedra (INESC-ID and Instituto Superior Técnico), 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.

Congratulations to all the team! I am looking forward to continuing our work in this very exciting area.

Here’s a photo of myself with Yuriy, Kyle, Alex, and Emily receiving the award:

Related News and Mentions

• INESC-ID researchers receive ACM SIGSOFT Distinguished Paper Award at ICSE 2025
• Prize ACM SIGSOFT Distinguished Paper for paper at ICSE 2025
• Software Reliability Lab announcement