Abstract
Oggi il software è presente in ogni aspetto della nostra vita: gestisce le comunicazioni, i servizi sanitari, i trasporti, la finanza, le infrastrutture energetiche e i sistemi di intelligenza artificiale. Per questo motivo, garantire che i programmi siano sicuri e corretti rappresenta una delle principali sfide della società digitale. Il progetto RAP affronta questa sfida sviluppando nuovi metodi matematici e informatici per analizzare il comportamento dei programmi tenendo conto di una risorsa spesso trascurata: il modo in cui dati, informazioni e capacità di calcolo vengono utilizzati, condivisi e consumati. In altre parole, il progetto considera i dati non come entità astratte, ma come risorse con un costo, un valore e un impatto concreto. Questa prospettiva permette di affrontare problemi di grande rilevanza sociale. Tra questi vi sono la tutela della privacy, la prevenzione della diffusione non autorizzata di informazioni sensibili, la verifica dell'affidabilità dei sistemi software e la riduzione del consumo energetico delle applicazioni informatiche. Diventa così possibile progettare strumenti in grado di certificare automaticamente il rispetto di determinati requisiti oppure di individuare in anticipo possibili errori, vulnerabilità o inefficienze. Le ricadute sono molteplici. Per i cittadini, software più affidabili significa maggiore tutela dei dati personali, servizi digitali più sicuri e tecnologie più trasparenti. Per le imprese, significa poter sviluppare applicazioni più robuste, riducendo i costi legati agli errori e aumentando la fiducia nei prodotti digitali. Per la pubblica amministrazione e gli enti che gestiscono servizi essenziali, significa disporre di strumenti avanzati per verificare la correttezza e la sicurezza dei sistemi su cui si basano attività fondamentali per la collettività. Il progetto RAP mira a porre le basi scientifiche per una nuova generazione di tecnologie digitali più sicure, affidabili, sostenibili e rispettose della privacy, contribuendo alla costruzione di una società sempre più capace di utilizzare il software in modo consapevole e responsabile.
Risultati raggiunti
Il progetto RAP ha prodotto risultati scientifici di assoluto rilievo internazionale, contribuendo in modo significativo allo sviluppo delle basi teoriche del resource-aware programming. Le attività di ricerca hanno permesso di conseguire risultati originali lungo l'intera filiera che va dai fondamenti matematici della programmazione fino allo sviluppo di nuove tecniche per l'analisi automatica del software, con applicazioni ai sistemi distribuiti, all'intelligenza artificiale e al calcolo quantistico. Un primo insieme di risultati ha riguardato lo sviluppo di nuovi modelli semantici e logici per la descrizione dei programmi e delle risorse computazionali. In particolare, il progetto ha esteso la teoria degli string diagrams, delle categorie monoidali e delle relazioni logiche quantitative, introducendo nuovi strumenti matematici per rappresentare programmi probabilistici, ragionare sul comportamento di programmi di ordine superiore e modellare in modo uniforme fenomeni quali probabilità, dipendenze contestuali e consumo di risorse. Questi contributi rafforzano in maniera sostanziale le basi teoriche della semantica dei linguaggi di programmazione e aprono nuove prospettive per la progettazione di sistemi di verifica fondati su solide strutture matematiche. Un secondo filone di ricerca ha riguardato la progettazione di nuove tecniche di analisi statica e verifica del software. Sono stati sviluppati innovativi sistemi logici capaci di combinare ragionamenti di correttezza e scorrettezza, permettendo non solo di individuare automaticamente errori realmente raggiungibili durante l'esecuzione dei programmi, ma anche di ricostruirne le cause e gli input che li generano. Parallelamente sono stati ottenuti risultati significativi nell'ambito dell'interpretazione astratta, del model checking e dell'approssimazione semantica, sviluppando nuovi metodi che migliorano la precisione delle analisi, riducono i falsi positivi e consentono di progettare strumenti di verifica più scalabili ed efficaci per sistemi software complessi. Il terzo filone ha esteso queste metodologie a domini di grande attualità, quali l'intelligenza artificiale e il calcolo quantistico. Il progetto ha prodotto nuovi modelli per analizzare la robustezza e la sensibilità delle reti neurali profonde, nuove basi matematiche per modelli interpretabili di intelligenza artificiale e nuovi metodi di analisi statica per programmi e circuiti quantistici, affrontando problemi quali il consumo di risorse, la sicurezza e la verifica formale di algoritmi quantistici. Tali risultati hanno inoltre portato allo sviluppo di strumenti prototipali, come il sistema QuRA, destinato al ragionamento quantitativo sui programmi quantistici. L'attività di ricerca si è caratterizzata per una forte integrazione tra le quattro unità coinvolte, che hanno sviluppato numerose collaborazioni scientifiche e prodotto risultati congiunti, favorendo la convergenza tra semantica dei linguaggi di programmazione, teoria delle categorie, interpretazione astratta, logiche dei programmi e metodi formali. L'eccellenza dei risultati conseguiti è testimoniata dalla qualità della produzione scientifica. Nel corso del progetto sono stati pubblicati o accettati numerosi articoli nelle più prestigiose conferenze e riviste internazionali del settore, tra cui POPL, LICS, CONCUR, FSCD, FOSSACS, CSL, VMCAI, SAS, OOPSLA, nonché sulle principali riviste dell'area, quali ACM Transactions on Programming Languages and Systems (TOPLAS), ACM Transactions on Computational Logic (TOCL), Theoretical Computer Science (TCS). La presenza continuativa in queste sedi, caratterizzate da procedure di selezione estremamente competitive e riconosciute come riferimento mondiale per l'informatica teorica e i linguaggi di programmazione, conferma l'elevato impatto scientifico del progetto RAP e la sua capacità di produrre risultati originali e di frontiera.Project details
Unibo Team Leader: Ugo Dal Lago
Unibo involved Department/s:
Dipartimento di Informatica - Scienza e Ingegneria
Coordinator:
Università degli Studi di Padova(Italy)
Total Eu Contribution: Euro (EUR) 273.836,00
Total Unibo Contribution: Euro (EUR) 130.462,00
Project Duration in months: 27
Start Date:
30/11/2023
End Date:
28/02/2026
