Un gruppo di ricercatori USI premiato nell'ambito degli EASST Best Paper Awards

Un paper scritto in collaborazione dai gruppi di ricerca dei Professori Natasha Sharygina e Patrick Eugster, Professori ordinari presso la Facoltà di scenze informatiche dell'USI, e presentato in occasione dell'edizione 2025 dell'International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) è stato premiato tra gli EASST Best Paper Awards. Il riconoscimento è stato attribuito durante l'ETAPS.

Il paper, intitolato "Unsatisfiability Proofs for Horn Solving", è stato premiato nella categoria "Papers related to the systematic and rigorous engineering of software systems".

Il lavoro è frutto di una collaborazione tra Martin Blicha, Ricercatore presso Formal Verification Lab dell'USI guidato dalla Professoressa Natasha Sharygina, e Rodrigo Otoni, Ricercatore presso il Software Systems Lab dell'USI guidato dal Professor Eugster. Collaborano inoltre al progetto Matias Barandiaran Rivera, Jan Kofroň, il Professor Patrick Eugster e la Professoressa Natasha Sharygina.

Lo studio del gruppo di ricerca parte dalla considerazione che molti strumenti di verifica si affidano attualmente a solutori logici come motori di ragionamento backend. Nonostante il ruolo centrale, i bug non sono rari nelle complesse basi di codice di questi solutori. La validazione dei loro risultati è quindi fondamentale e a questo scopo vengono spesso utilizzati i testimoni di correttezza. La validazione dei risultati per i solutori di clausole di Horn vincolate (CHC) non è però un argomento ben esplorato, soprattutto per quanto riguarda i risultati di insoddisfacibilità. Si tratta di un problema significativo, dato che i solutori CHC sono sempre più utilizzati negli strumenti di verifica. Per risolvere questo problema, i ricercatori propongono un approccio per la validazione dei risultati di insoddisfacibilità dei CHC basato su prove verificabili in modo indipendente. L'approccio proposto è generico per quanto riguarda l'algoritmo risolutivo, le fasi di preelaborazione e il formato esatto della prova utilizzata, e funziona producendo prima una prova a grana grossa durante la risoluzione e poi istanziandola in un formato di prova adeguato aggiungendo i dettagli mancanti; a questo punto la prova istanziata può essere verificata da un verificatore di prove indipendente. È stato strumentato un solutore CHC all'avanguardia per generare prove nel formato Alethe ed è stata eseguita una valutazione su larga scala. I risultati ottenuti indicano che le prove possono essere prodotte con un overhead minimo, possono essere verificate in modo efficiente e hanno dimensioni ragionevoli.

TACAS è un forum per ricercatori, sviluppatori e utenti interessati a strumenti e algoritmi rigorosi per la costruzione e l'analisi dei sistemi. La conferenza mira a colmare le lacune tra le diverse comunità con questo interesse comune e a sostenerle nella loro ricerca di migliorare l'utilità, l'affidabilità, la flessibilità e l'efficienza degli strumenti e degli algoritmi per la costruzione di sistemi. La conferenza TACAS è un membro fondatore dell'ETAPS. Le sue radici risalgono al 1995, quando si tenne per la prima volta ad Aalborg, in Danimarca. Da allora gli atti del TACAS sono pubblicati nella serie LNCS di Springer-Verlag.

ETAPS è una confederazione di diverse conferenze, ognuna con un proprio comitato di programma e un comitato direttivo. L'ETAPS è il più importante e visibile evento annuale europeo relativo alle scienze del software. Complessivamente, ogni anno vi partecipano più di 500 ricercatori. L'assegnazione di ogni EASST Best Paper Award viene fatta da un comitato selezionato, che decide ogni anno il vincitore del premio.

È possibile leggere il paper al seguente link.