Trasformatori di completezza e Non-Interferenza astratta: Nuovi approcci per l'analisi dei Programmi

Questa presentazione si concentrata fondamentalmente su due lavori indipendenti, ma allo stesso tempo correlati: l'approfondimento della nozione di non interferenza astratta e i trasformatori di completezza. La non interferenza e' una proprieta' della semantica dei programmi originariamente sviluppata nel contesto della sicurezza dei linguaggi. In questo ambito abbiamo quindi indebolito questo concetto introducendo la non interferenza astratta, studiandola approfonditamente al fine di comprendere meglio il problema della non interferenza ed estendere e collegare il framework sviluppato ad ambiti differenti dalla sicurezza, quali ad esempio lo slicing di programmi.
La completezza e' una proprieta' dei domini astratti che permette di valutare quanto preciso sia il dato dominio per la computazione di una semantica. In altre parole un dominio e' completo per una semantica se contiene tutta l'informazione necessaria per una precisa computazione della semantica, ovvero se non ha eliminato troppa informazione concreta. I trasformatori di completezza sono trasformatori che permettono di modificare un dato dominio o una data semantica in modo da rendere il dominio completo per la semantica. I trasformatori di domini si sono rivelati utili in diversi ambiti dell'informatica, come il model checking e l'analisi statica in generale. Qui mostriamo come abbiamo utilizzato questi trasformatori anche nell'ambito della non interferenza astratta, da cui il collegamento tra i due argomenti trattati. Inoltre mostriamo la costruzione di trasformatori di completezza che modificano le semantiche invece dei domini. Questi nuovi studi sono interessanti non solo nel contesto della non interferenza astratta ma anche in contesti differenti quali l'offuscamento e il watermarking di programmi.