Obiettivi formativi
<span class="datirigaalto"><span class="datirigaalto">La crescente dipendenza della società dalle applicazioni<br />
informatiche fa sí che l'analisi e la verifica della<br />
correttezza dei sistemi complessi rappresenti sempre di<br />
più un fattore critico del processo di sviluppo.<br />
Il malfunzionamento dei sistemi, siano essi hardware,<br />
software o protocolli di comunicazione, può comportare<br />
danni rilevanti di ogni genere: dalla perdita finanziaria<br />
alla perdita di vite umane. Inoltre, quando i difetti non<br />
sono rilevati prima dell'impiego del sistema,<br />
l'applicazione di eventuali misure correttive è, quando<br />
possibile, ben più difficile e costosa. Esempi dal recente<br />
passato includono il millennium bug, gli errori<br />
di alcune versioni del processore Pentium, lo<br />
scoperto da 32 miliardi di dollari alla N.Y. Bank,<br />
il fallimento iniziale del vettore Ariane 5, e<br />
gli incidenti mortali del Therac-25.<br />
<br />
Il corso intende fornire una prima introduzione alle<br />
tecniche che stanno alla base dell'analisi automatica<br />
del software e della verifica formale assistita dal<br />
calcolatore. </span></span>