arXiv subjects

Martim Afonso

Publications and source records attributed to Martim Afonso.

3 recordsLinked to original sources

arXiv2026

VerusWeave: A Benchmark for Proof Repair in Concurrent Verus Programs

Concurrent software underpins critical infrastructure, including operating systems and databases, yet thread interactions can have bugs that bypass conventional testing. Verus extends Rust with formal verification capabilities, enabling developers to specify, implement and prove the correctness of concurrent code in the same language. Although coding agents have been explored for automated proof construction, existing Verus benchmarks offer limited coverage of concurrency-specific examples that connect atomic operations to abstract protocols. To address this gap, we introduce VerusWeave, the first benchmark dedicated to concurrent proof repair, derived from four open-source projects. It comprises 75 focused tasks and 17 full-module variants that exercise features used to verify low-level concurrent code. Tasks remove selected proof annotations and require agents to fill gaps, while preserving executable code and specifications. The evaluation harness validates repairs using Verus and a change checker, recording solutions, execution traces, and resource usage. An initial evaluation of four general-purpose coding-agent harnesses achieved 75-85% success on focused tasks and 29-47% on full-module variants, highlighting the challenge of autonomous module-wide repairs. VerusWeave provides a reusable foundation for evaluating automated proof construction for concurrent software.

cs.SE↗

arXiv2026

ProfOlaf: Semi-Automated Tool for Systematic Literature Reviews

Systematic reviews and mapping studies are critical to synthesize research, identify gaps, and guide future work, but are often labor-intensive and time-consuming. Existing tools provide partial support for specific steps, leaving much of the process manual and error-prone. We present ProfOlaf, a semi-automated tool designed to streamline systematic reviews while maintaining methodological rigor. ProfOlaf supports iterative snowballing for article collection with human-in-the-loop filtering and uses large language models to help select articles, extract key topics, and answer queries about the content of articles. By combining automation with guided manual effort, ProfOlaf enhances the efficiency, quality, and reproducibility of systematic reviews across research fields. ProfOlaf can be used both as a CLI tool and in web application format. A video demonstrating ProfOlaf is available at: https://youtu.be/R-gY4dJlN3s

cs.IR↗

arXiv2024

Finding Regions of Interest in Whole Slide Images Using Multiple Instance Learning

Whole Slide Images (WSI), obtained by high-resolution digital scanning of microscope slides at multiple scales, are the cornerstone of modern Digital Pathology. However, they represent a particular challenge to AI-based/AI-mediated analysis because pathology labeling is typically done at slide-level, instead of tile-level. It is not just that medical diagnostics is recorded at the specimen level, the detection of oncogene mutation is also experimentally obtained, and recorded by initiatives like The Cancer Genome Atlas (TCGA), at the slide level. This configures a dual challenge: a) accurately predicting the overall cancer phenotype and b) finding out what cellular morphologies are associated with it at the tile level. To address these challenges, a weakly supervised Multiple Instance Learning (MIL) approach was explored for two prevalent cancer types, Invasive Breast Carcinoma (TCGA-BRCA) and Lung Squamous Cell Carcinoma (TCGA-LUSC). This approach was explored for tumor detection at low magnification levels and TP53 mutations at various levels. Our results show that a novel additive implementation of MIL matched the performance of reference implementation (AUC 0.96), and was only slightly outperformed by Attention MIL (AUC 0.97). More interestingly from the perspective of the molecular pathologist, these different AI architectures identify distinct sensitivities to morphological features (through the detection of Regions of Interest, RoI) at different amplification levels. Tellingly, TP53 mutation was most sensitive to features at the higher applications where cellular morphology is resolved.

cs.CV↗