Maria Paola Bonacina vince per la seconda volta l’Amazon Research Award

Maria Paola Bonacina, docente del dipartimento di Informatica del nostro ateneo, ha vinto per la seconda volta un Amazon Research Award (Ara) nella categoria ragionamento automatico, con un progetto intitolato “New Data Structure Theories and Quantifiers in CDSAT“

In questo progetto Maria Paola Bonacina investigherà la modellazione di strutture di dati e il ragionamento sui quantificatori (per ogni, esiste) in soddisfacibilità modulo teorie (SMT). Teorie espressive per le strutture di dati e metodi efficienti per ragionare sui quantificatori sono elementi essenziali per la verifica automatica dei programmi. Per esempio gli array sono ubiqui in  programmazione e si usano anche per ragionare sulla memoria del computer (lo heap).
Tuttavia, la loro teoria non definisce caratteristiche come la lunghezza o operazioni come la concatenazione. Quindi si definiranno nuove teorie che superino tali limitazioni per gli array e i vettori (array dinamici).

Il metodo CDSAT (Conflict-Driven Satisfiability) sarà applicato alle nuove teorie, e combinato con l'algoritmo QSMA (Quantified Satisfiability Modulo Assignment) per i quantificatori. CDSAT e QSMA sono risultati di precedenti ricerche di Maria Paola Bonacina.

“L'Amazon Research Award, spiega Maria Paola Bonacina, è importante per parecchie ragioni. È un premio internazionale per il quale competono ricercatori e ricercatrici da tutto il mondo. Viene messo in palio da un'azienda leader globale in informatica con forti competenze interne e investimenti nella ricerca. Infine, premia la ricerca individuale, anche se la collaborazione è naturalmente permessa.”

“Vincere l'Amazon Research Award e vincerlo per la seconda volta, aggiunge la docente, è una grande soddisfazione. È un riconoscimento alla continuità e alla persistenza nella ricerca di alto livello. Non sono certo molte le persone che lo abbiano vinto due volte e in un campo competitivo come il ragionamento automatico”.