Analisi della verifica di programmi C attraverso il software Frama-C

In questo trattato ho approfondito il tema della verifica formale, prima da un punto di vista teorico e successivamente da un punto di vista pratico. La trattazione della teoria accenna solo ad alcune delle nozioni fondamentali per la comprensione della verifica formale ed il loro approfondimento é lasciato ad articoli che ne approfondiscono piú chiaramente e piú dettagliatamente i vari aspetti. La trattazione pratica prevede invece lo sviluppo della verifica di alcuni algoritmi fondamentali quali algoritmi di ricerca e di ordinamento tramite lo strumento Frama-C.