Metodi formali

Esploreremo delle tecniche formali per migliorare
l'affidabilità del software, concentrandoci in particolare sulla
specifica e dimostrazione di proprietà del software.

La particolarità di questa parte è di essere costruita interamente
all'interno di Coq, uno dei proof assistant (p.a.) più maturi ed
usati. Un p.a. è uno esempio di dimostratore di teoremi interattivo,
che cioè automatizza gli aspetti più di routine della dimostrazione ma
dipende dall'utente per la strategia dimostrativa. Insegnamento
esercizi ed esame compresi, vanno quindi (e)seguito come una sessione
interattiva con il sistema.
https://softwarefoundations.cis.upenn.edu/

Gli argomenti principali che svilupperemo saranno:

(1) (Ri)esame di alcuni strumenti basi logici per la specifica e
dimostrazione delle proprietà di interesse (induzione, ricorsione,
riscrittura).

(2) Uso dei p.a. nella costruzione di argomenti logici rigorosi.

(3) La programmazione funzionale sia come metodologia di
programmazione che come ponte con la logica.

(4) Tecniche formali per il ragionamenti sulle proprietà di programmi
specifici (terminazione di un loop, dimostrazione che una funzione di
sorting soddisfa la sua specifica) via le logiche di Hoare

(5) per la dimostrazione di proprietà di tutti i programmi di un certo
linguaggio. Esamineremo il lambda calcolo tipato e le sue proprietà come la correttezza dei tipi

Infine guarderemo alcuni argomenti di ricerca corrente connessi alla automazione di queste argomenti via
i . collegamento con dimostratori automatici (CoqHammer)
ii. tecniche di machine learning