João F. Ferreira, INESC-ID researcher and professor at the Department of Computer Science and Engineering (DEI) at Instituto Superior Técnico, and Nuno Saavedra, PhD student and INESC-ID researcher, have received the prestigious ACM SIGSOFT Distinguished Paper Award at the International Conference on Software Engineering (ICSE) 2025—the premier global event in software engineering.

The award-winning paper, titled “Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification,” presents a novel approach to proof synthesis using machine learning and large language models (LLMs), enhanced by retrieval augmentation techniques. Rango introduces a dynamic, adaptive system that identifies and integrates relevant proofs and premises at each stage of the software verification process. This allows the tool to tailor its reasoning to both the specific project and the evolving state of the proof itself.

The effectiveness of Rango was demonstrated using a newly curated dataset, CoqStoq, which contains more than 2,200 open-source Coq projects. The tool successfully synthesized proofs for 32% of theorems, marking a 29% improvement over previous state-of-the-art systems—an impressive leap forward that could help make formal software verification more accessible and practical for developers.

This significant achievement is the result of a strong international collaboration with the research including researchers from the University of California San Diego, the University of Massachusetts and Pedro Carrott, a former MSc student at Técnico, supervised by João F. Ferreira and presently at Imperial College London.

The ACM SIGSOFT Distinguished Paper Award is reserved for papers of exceptional quality presented at ICSE, and this recognition reflects both the scientific impact and collaborative excellence behind the work.