Related Experiment Video For Formal methods
Updated: Nov 23, 2025
Detection and Isolation of Cancer in Prostate Biopsies Using Stimulated Raman Histology and Artificial Intelligence
Published on: June 10, 2025
Radiomic features for prostate cancer grade detection through formal verification
Antonella Santone1, Maria Chiara Brunese1, Federico Donnarumma1
1Department of Medicine and Health Sciences "Vincenzo Tiberio", University of Molise, Campobasso, Italy.
Aim:
Prostate cancer represents the most common cancer afflicting men. It may be asymptomatic at the early stage. In this paper, we propose a methodology aimed to detect the prostate cancer grade by computing non-invasive shape-based radiomic features directly from magnetic resonance images.
Materials And Methods:
We use a freely available dataset composed by coronal magnetic resonance images belonging to 112 patients. We represent magnetic resonance slices in terms of formal model, and we exploit model checking to check whether a set of properties (formulated with the support of pathologists and radiologists) is verified on the formal model. Each property is related to a different cancer grade with the aim to cover all the cancer grade groups.
Results:
An average specificity equal to 0.97 and an average sensitivity equal to 1 have been obtained with our methodology.
Conclusion:
The experimental analysis demonstrates the effectiveness of radiomics and formal verification for Gleason grade group detection from magnetic resonance.
