Introduzione ai metodi formali nel software e nei servizi. Uso di logiche per esprimere specifiche e proprietà statiche e dinamiche: logica del prim'ordine, query al prim'ordine, query congiuntive. logiche descrittive, logiche temporali e logiche dinamiche.
Metodi formali: analisi e verifica di aspetti statici.
Sintassi e semantica formale dei diagrammi concettuali, quali diagrammi delle classi UML e diagrammi Entità Relazione, verifica di proprietà statiche, uso di logica del prim'ordine e di logiche descrittive per il ragionamento automatico su tali diagrammi. Interrogazioni su diagrammi UML. Uso delle logiche descrittive, ALC, ALCQI, DL-LiteA. Ragionamento su logiche descrittive: procedure basate su tableaux per ALC. Query answering di query congiuntive (e unioni di query congiuntive) in logiche descrittive: procedure basate su perfect-rewriting in DL-LiteA.
Metodi formali: analisi e verifica di aspetti dinamici.
Semantica operazionale astratta dei programmi: semantica di valutazione (intera computazione) e semantica di transizione (singolo passo della computazione). Precondizioni, postcondizioni e invarianti di un programma. Correttezza parziale e totale. Programmi reattivi/interattivi (a stati finiti) reattivi come sistemi di transizione (cf. semantica di transizione), astrazione. Punti fissi, teorema di Knaster-Tarski su least e greatest fixpoint, approssimanti di least e greatest fixpoint. Verifica di proprietà dinamiche e temporali su sistemi di transizione: Safeness, Liveness, Fairness, Strong Fairness. Logiche temporali per la verifica: LTL, CTL, CTL*, mu-calculus. Model checking per CTL. Model checking per mu-calculus. Model checking per LTL.