Speaker: Lorenzo Lago, Università degli Studi di Milano

Le attuali memorie, soprattutto quelle più economiche e veloci, sono caratterizzate da tassi di errore non trascurabili. Se consideriamo sistemi che necessitano di una gran quantità di memoria la probabilità che avvenga un errore non può sicuramente essere sottovalutato. Poiché la correttezza degli algoritmi risulta vanificata anche da errori su pochi bit di memoria, la possibilità di calcolare correttamente anche in presenza di dati corrotti diventa fondamentale per molte applicazioni. Qualora non sia possibile, o sia troppo costoso, ricorrere ad hardware specifico per la rilevazione e la correzione degli errori, è ragionevole cercare una soluzione a questo problema a livello applicativo, ovvero progettare algoritmi e strutture dati capaci di garantire soluzioni corrette anche in presenza di informazioni inaffidabili o corrotte.

Gli OBDD (Ordered Binary Decision Diagram) sono strutture dati utilizzate per rappresentare funzioni booleane in modo efficiente, sia dal punto di vista delle operazioni tra funzioni, sia per quanto riguarda lo spazio di memoria utilizzato. Un OBDD è un grafo diretto aciclico (DAG), nel quale ogni nodo è composto da un indice, che indica una variabile della funzione, e da due puntatori a due sottografi. L'utilizzo degli OBDD spazia dalla sintesi logica alla verifica formale. Durante il seminario verranno descritte alcune strategie per rendere gli OBDD resilienti agli errori, utilizzando sia la loro ridondanza intrinseca che quella introdotta dalle loro implementazioni efficienti, e cercando soluzioni adatte ad essere applicate a pacchetti per la gestione di OBDD già esistenti.

(Referente: Anna Bernasconi- Dip. Informatica, UniPi)