Searcharxiv⌕ Search

arXiv subjects

Ana Ribeiro

Publications and source records attributed to Ana Ribeiro.

6 recordsLinked to original sources
arXiv2026

Systematic API Testing Through Model Checking and Executable Contracts

Automated black-box testing of APIs typically relies on interface specifications that define available operations and data schemas, but offer limited or no behavioural semantics. This semantic gap amplifies the test-oracle problem and limits the generation of effective, stateful call sequences. We introduce IcePick, a framework that achieves systematic state-space coverage for API testing by leveraging model checking. IcePick uses TLA+ to formally model API state evolution, employs the TLC model checker to exhaustively explore reachable states, and generates test sequences that provably cover the behavioural model. To mitigate state-space explosion and improve sequence extraction, we introduce a coverage-guided breadth-first traversal of the TLC state-space graph. To address oracle limitations beyond HTTP status codes, we propose Glacier, a first-order logic contract language that enriches API specifications with executable semantic contracts, enabling automated behavioural verification during test execution. We evaluate IcePick on EvoMaster Benchmark systems, demonstrating that model-checking-guided exploration achieves complete state coverage and reveals faults in multi-operation interactions. We also analyse scalability to characterise practical limits and applicability requirements. Overall, IcePick provides reproducible test suites with strong coverage guarantees for critical API-based systems.

cs.SE↗
arXiv2025

AI-driven software for automated quantification of skeletal metastases and treatment response evaluation using Whole-Body Diffusion-Weighted MRI (WB-DWI) in Advanced Prostate Cancer

Quantitative assessment of treatment response in Advanced Prostate Cancer (APC) with bone metastases remains an unmet clinical need. Whole-Body Diffusion-Weighted MRI (WB-DWI) provides two response biomarkers: Total Diffusion Volume (TDV) and global Apparent Diffusion Coefficient (gADC). However, tracking post-treatment changes of TDV and gADC from manually delineated lesions is cumbersome and increases inter-reader variability. We developed a software to automate this process. Core technologies include: (i) a weakly-supervised Residual U-Net model generating a skeleton probability map to isolate bone; (ii) a statistical framework for WB-DWI intensity normalisation, obtaining a signal-normalised b=900s/mm^2 (b900) image; and (iii) a shallow convolutional neural network that processes outputs from (i) and (ii) to generate a mask of suspected bone lesions, characterised by higher b900 signal intensity due to restricted water diffusion. This mask is applied to the gADC map to extract TDV and gADC statistics. We tested the tool using expert-defined metastatic bone disease delineations on 66 datasets, assessed repeatability of imaging biomarkers (N=10), and compared software-based response assessment with a construct reference standard (N=118). Average dice score between manual and automated delineations was 0.6 for lesions within pelvis and spine, with an average surface distance of 2mm. Relative differences for log-transformed TDV (log-TDV) and median gADC were 8.8% and 5%, respectively. Repeatability analysis showed coefficients of variation of 4.6% for log-TDV and 3.5% for median gADC, with intraclass correlation coefficients of 0.94 or higher. The software achieved 80.5% accuracy, 84.3% sensitivity, and 85.7% specificity in assessing response to treatment. Average computation time was 90s per scan.

cs.LG↗
arXiv2024

3D Modelling to Address Pandemic Challenges: A Project-Based Learning Methodology

The use of 3D modelling in medical education is a revolutionary tool during the learning process. In fact, this type of technology enables a more interactive teaching approach, making information retention more effective and enhancing students' understanding. 3D modelling allows for the creation of precise representations of the human body, as well as interaction with three-dimensional models, giving students a better spatial understanding of the different organs and systems and enabling simulations of surgical and technical procedures. This way, medical education is enriched with a more realistic and safe educational experience. The goal is to understand whether, when students and schools are challenged, they play an important role in addressing health issues in their community. School-led projects are directed towards educational scenarios that emphasize STEM education, tackling relevant public health problems through open-school initiatives. By implementing an educational scenario focused on 3D modelling and leveraging technology, we aim to raise community awareness on public health issues.

cs.MM↗
arXiv2023

JepREST: Functional tests for distributed REST applications

Application services often support mobile and web applications with REST interfaces, implemented using a set of distributed components that interact with each other. This approach allows services to have high availability and performance at a lower cost than a monolithic system. However, the existence of multiple components makes the development process of these systems more complex and therefore susceptible to errors. In this paper, we present JepREST, a system that automates the use of Jepsen libraries to test the correctness of distributed applications that provide a REST interface. Based on a service interface specification, JepREST generates and executes a set of tests with multiple clients performing operations concurrently, subsequently verifying if the system behaviour is linearizable. The preliminary evaluation shows that JepREST simplifies the testing of REST applications.

cs.DC↗