Metodi formali

A.A. 2024/2025
6
Crediti massimi
48
Ore totali
SSD
INF/01
Lingua
Italiano
Obiettivi formativi
L'insegnamento intende esplorare le tecniche formali per migliorare l'affidabilità del software, con un focus particolare sulla specifica e dimostrazione di proprietà del software. Gli strumenti scelti sono i model checker simbolici e la della dimostrazione assistita dal calcolatore.
Risultati apprendimento attesi
Lo studente sarà in grado di modellare e dimostrare la correttezza di semplici proprietà del software usando un insieme di tools presentati nelle ore di laboratorio.
Corso singolo

Questo insegnamento può essere seguito come corso singolo.

Programma e organizzazione didattica

Edizione unica

Periodo
Primo semestre

Programma
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
Prerequisiti
E' richiesta la conoscenza di nozioni basi di logica, meglio se avendo superato l'esame di logica magistrale. Sarebbe utile (ma non necessaria) esperienza con programmazione funzionale
Metodi didattici
Lezioni frontali e laboratorio
Materiale di riferimento
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame (valutato in trentesimi) consiste in una prova di laboratorio di durata di 3 (tre) ore, in cui si usano gli strumenti software spiegati a lezione e nelle esercitazioni. Eccezionalmente, si può concordare un breve progetto per migliorare il voto finale

E' possibile un progetto di approfondimento su un argomento concordato col docente
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
Turni:
Docente/i
Ricevimento:
su appuntamento
4009, Celoria 18