Metodi Formali 2020/21

Il corso si propone di offrire agli studenti le conoscenze di base relative ai metodi logico matematici per l'analisi e la verifica formale di proprietà dei programmi. A questo scopo, dopo aver trattato di sistemi equazionali, riscrittura, logica e λ-calcolo, vengono introdotte le basi teoriche della semantica dei programmi e della logica di Floyd-Hoare. Inoltre saranno introdotte tecniche di analisi statica di programmi con puntatori basate sulla Separation logic.

Il corso introduce all'uso di proof-assistant per l'analisi di programmi assistita da calcolatore, quali Agda e VeriFast.


Calcolabilità e Complessità 2020

Prerequisiti

Il corso richiede conoscenze di logica, programmazione e di algoritmi; inoltre si assume che lo studente possegga le nozioni di linguaggio formale, grammatica e di automa, gli argomenti svolti negli esami: Matematica Discreta e Logica, Programmazione 1 e 2, Algoritmi e Strutture Dati, Linguaggi Formali e Traduttori.


Argomenti del corso

Il Corso affronta i seguenti problemi: che cos'e' un algoritmo? Quali problemi si possono risolvere con un algoritmo? E in quali casi un algoritmo richiede risorse inaccessibili nella pratica? Affrontare questi problemi richiede definire la nozione di macchine di Turing, di funzioni calcolabile, i vari possibili criteri di misura delle risorse disponibili (tempo, memoria, processori), le classi di complessita' e il problema P = NP. L'obbiettivo e' imparare la definizione del concetto di calcolo, una maggiore consapevolezza delle limitazioni intrinseche all'uso delle macchine, ed un'idea delle strategie per aggirare a tali limitazioni.


Modalità del corso

Le lezioni si svolgono in aula, ed utilizzano Moodle sia per inviare  messaggi agli studenti che per descrivere sezioni ed esercizi svolti.


Libro di testo e Dispense

Il libro di testo del corso e' il seguente: M. Sipser:"Introduction to the theory of Computation", Course Technology Ptr., 3^edition, 2012. Svolgeremo parte delle sezioni 3,4,5 della parte 2 (Calcolabilità), tranne i risultati sulle grammatiche, e una parte da definire della parte 3 (Complessità). Per maggiori dettagli si veda il programma di esame.



Piano del corso.

48 ore e 24 lezioni di 2 ore ciascuna.

 

Programma tradizionale.

Chiediamo le dimostrazioni di 3 enunciati: Indecidibilità della Accettazione (4.11: linee generali), Teorema 4.22 (detto anche T. di Post), CLIQUE è NP-completo (7.32). In tutti gli altri casi viene richiesto il solo enunciato.

 

Teoria della Computabilità

    • Le Macchine di Turing deterministiche, a più registri, non deterministiche (§ 3).
    • Problemi con soluzione non calcolabile: prova (linee generali) che il problema della accettazione non è decidibile (§ 4 da 4.2). Prova del T. 4.22 (detto anche T. di Post).

 

Teoria della Complessità

    • Classi di Complessita' Temporale (§ 7): definizioni P, NP, EXPTIME, inclusioni note e congetturate, NP-completezza (7.34), Enunciato del Teorema di Cook (7.27).
    • Problemi NP-completi: enunciato problema del cammino di Hamilton e problema SUBSETSUM (sez. 7.3), prova che CLIQUE è NP-completo (7.32).