Implementazione e Dimostrazione del Nucleo di VeriFast utilizzando Isabelle​

Isabelle è un potente programma per la dimostrazione formale di teoremi formalizzati secondo il paradigma funzionale. Esso ci per- mette di formalizzare il nucleo dei comandi di VeriFast, un altro lin- guaggio per la dimostrazione di programmi che seguono il paradigma imperativo. Nel corso di questa tesi andremo a implementare i vari comandi che compongoo il nucleo di VeriFast utilizzando Isabelle, di- mostrando importanti lemmi su di essi. nella seconda parte utilizzer- emo la semantica Big Step per dimostrare che i comandi che abbiamo formalizzato sono corretti, mentre nell'ultima parte utilizzeremo la se- matica Smal Step, oltre che per dimostrare la correttezza di quanto abbiamo scritto e formulato, per verificare che le due semantiche, in relazione al nucleo di VeriFast sono identiche.