Qed in libertà: Un'indagine sull'ingegneria del software formalmente verificato

Titolo originale:

Qed at Large: A Survey of Engineering of Formally Verified Software

Contenuto del libro:

Lo sviluppo di prove formali di correttezza dei programmi può aumentare l'affidabilità reale e percepita e facilitare una migliore comprensione delle specifiche dei programmi e delle loro ipotesi sottostanti. Gli strumenti che supportano questo tipo di sviluppo sono disponibili da oltre 40 anni, ma solo di recente hanno visto un ampio utilizzo pratico.

I progetti basati sulla costruzione di prove formali controllate meccanicamente stanno ora raggiungendo una scala senza precedenti, paragonabile a quella dei grandi progetti software, il che porta a nuove sfide nello sviluppo e nella manutenzione delle prove. Nonostante la sua crescente importanza, il campo dell'ingegneria delle prove è raramente considerato a sé stante; le teorie, le tecniche e gli strumenti correlati abbracciano molti campi e sedi. QED at Large copre la letteratura temporale e di ricerca riguardante lo sviluppo di prove per la verifica dei programmi, comprese le teorie, i linguaggi e gli strumenti.

La monografia sottolinea le sfide e i progressi compiuti in ogni fase della storia e mette in evidenza le sfide che si presentano attualmente a causa della crescente scala degli sviluppi delle prove. Questa monografia è destinata a ricercatori e studenti alle prime armi.

Fornisce al lettore una panoramica approfondita del lavoro che ha portato alle moderne tecniche di verifica formale del software. In tempi di crescente automazione, queste tecniche sono alla base di molti sistemi software, per cui vengono evidenziate anche le tendenze future.