FORMAL METHODS

Obiettivi formativi

Obiettivi generali: L'obiettivo del corso è lo studio e l'approfondimento della qualità più importante del software: la correttezza. Lo studio della correttezza verrà affrontato con riferimento ad aspetti concettuali e realizzativi affrontando la modellazione e la verifica sia di aspetti statici che di aspetti dinamici. Gli argomenti vengono trattati dando enfasi ad aspetti metodologici e ad aspetti sperimentali utilizzando varie forme di logica (logica del prim'ordine, logiche dinamiche e logiche temporali) e vari strumenti per la verifica automatica. Risultati di apprendimento attesi: Alla fine del corso lo studente dovrebbe avere acquisito tecniche e metodi per la dimostrazione della correttezza dei programmi e degli schemi concettuali. Obiettivi specifici: Conoscenza e comprensione: I principali fondamentali dei metodi formali. L'uso di specifiche rigorose e formali e la loro verifica. Principi fondanti della logica per l'informatica, verifica formale di proprieta' dei dati e dei processi. Applicare conoscenza e comprensione: Essere in grado di affrontare l'analisi di correttezza di programmi attraverso metodi rigorosi e formali, sia relativamente ad aspetti relativi ai dati che ai processi. Capacità critiche e di giudizio: Essere in grado di valutare il rigore di una data argomentazione di correttezza dei programmi. Orientarsi nella scelta degli strumenti concettuali forniti dalla logica e i metodi formali per la verifica di proprieta' sia statiche che dinamiche. Capacità comunicative: Le attività di gruppo in classe e le esercitazioni del corso permettono allo studente di essere in grado di comunicare/condividere le conoscenze acquisite e confrontarsi con gli altri sui temi del corso. Capacità di apprendimento: Oltre alle classiche capacità di apprendimento fornite dallo studio teorico del materiale didattico, le modalità di svolgimento del corso, stimolano lo studente all'approfondimento autonomo di alcuni argomenti presentati nel corso, al lavoro di gruppo, e all'applicazione concreta delle nozioni e delle tecniche apprese durante il corso.

Canale 1
GIUSEPPE DE GIACOMO Scheda docente

Programmi - Frequenza - Esami

Programma
Introduzione. Introduzione ai metodi formali, garanzie formali, revisione della logica proposizionale e della logica del primo ordine, verifica del modello/interrogazione e ragionamento (soddisfacibilità, validità e implicazione logica). Tableau per la logica proposizionale e del primo ordine. Analisi e verifica degli aspetti statici. Sintassi e semantica dei diagrammi concettuali basati su classi come i diagrammi delle classi UML e i diagrammi entità-relazioni. Verifica delle proprietà statiche. Uso della logica del primo ordine per il ragionamento automatizzato su tali diagrammi. Chase per dipendenze complete per completare le istanze dei diagrammi delle classi UML. Semantica operazionale astratta e correttezza parziale. Semantica operazionale astratta per i programmi: semantica di valutazione (calcolo completo) e semantica di transizione (singolo passo del calcolo). Logiche di Hoare, precondizione più debole, invarianti dei programmi. Correttezza parziale, correttezza totale. Sistema di transizione e punti fissi. Programmi reattivi/interattivi (stato finito), sistemi di transizione, raggiungibilità, bisimulazione. Punti fissi, teorema di Knaster-Tarski sui punti fissi minimi e massimi, approssimazioni per i punti fissi minimi e massimi. Verifica di sistemi dinamici. Verifica delle proprietà dinamiche e temporali sui sistemi di transizione: Safeness, Liveness, Fairness, Strong Fairness. Logica temporale per la verifica: LTL, CTL, CTL*, mu-calcolo. Verifica del modello per mu-calcolo. Verifica del modello per CTL tramite traduzione in μ-calcolo. Verifica del modello per LTL tramite automi. Soddisfacibilità LTL tramite Tableau. Focalizzarsi su tracce finite. Automi regolari, logiche temporali lineari su tracce finite, LTLf, LDLf, Pure Past LTL,, connessioni agli automi, calcolo degli DFA, manipolazione di DFA, ragionamento su tracce finite. Sintesi reattiva. Sintesi automatizzata dei programmi, sintesi da specifiche in logica temporale lineare su tracce finite, game-theoretic view, arena e obiettivo, adversarial reachability.
Prerequisiti
Gli studenti che seguono questo corso dovrebbero avere conoscenze di modellazione e progettazione del software, database relazionali e nozioni di base di logica proposizionale e del primo ordine acquisite nei corsi degli anni precedenti.
Testi di riferimento
Slide del corso 2025/2026 e materiale addizionale disponibili sulla pagina web del corso.
Frequenza
La frequenza non è obbligatoria, ma fortemente incoraggiata.
Modalità di esame
Prova scritta con esercizi su tutti gli argomenti del programma del corso.
Modalità di erogazione
Il corso è erogato attraverso lezioni frontali.
  • Codice insegnamento1038133
  • Anno accademico2025/2026
  • CorsoArtificial Intelligence – Intelligenza Artificiale
  • CurriculumCurriculum unico
  • Anno2º anno
  • Semestre1º semestre
  • SSDING-INF/05
  • CFU6