Corso di Metdodi per il Ragionamento Automatico

Prof. Silvio Ghilardi

Laurea Magistrale in Informatica - a.a. 2009/2010

AVVISI:

Le slides dell'intervento della prof. M. Heiner sono disponibili a questo link, nella sottodirectory ->publications->tutorials.

Le slides del corso di dottorato tenuto dal prof. De Moura (Microsoft Research, Redmond, USA) i cui argomenti hanno ampia intersezione con le tematiche affrontate nel corso di Metodi per il Ragionamento Automatico, sono disponibili sulla mia pagina web principale (sotto ->teaching).

Caratteristiche del corso | Programma del corso | Orari | Modalità d'esame | Materiali didattici | Appelli d'esame

  1. Caratteristiche del corso

    2. Questo corso, a differenza degli altri corsi di area logica, è direttamente incentrato su aspetti di sviluppo e di sperimentazione. Per questo motivo, è richiesta agli studenti una partecipazione attiva, dopo un breve periodo di training. L'intenzione è di discutere ed approntare assieme formalizzazioni di problemi di verifica, di sottoporle al model checker MCMT e di elaborare soluzioni idonee a livello di specifica, di impostazioni e di implementazione.

  2. Programma del corso

    3. Il corso si suddividerà in due tronconi, il primo riguardante gli SMT solvers e il secondo il model-checking a stati infiniti. Nella parte finale del corso si descriverà l'integrazione fra le due tematiche, così come si sta concretizzando nel sistema MCMT (Model Checker Modulo Theories), che è in corso di sviluppo.

    Programma della prima parte:
    1. richiami su concetti base di logica proposizionale e predicativa;
    2. problemi SAT, procedura DPLL;
    3. procedure di decisione per teorie significative (teoria dell'uguaglianza con simboli non interpretati, aritmetica lineare reale e intera, teoria degli array);
    4. integrazione delle procedure di decisione nell'algoritmo DPLL;
    5. il progetto SMT-LIB e gli SMT-solvers;
    6. introduzione al sistema Yices.

    Programma della seconda parte:
    1. il model-checking simbolico nei sistemi a stati finiti;
    2. risultati generali sui sistemi a stati infiniti "ben strutturati";
    3. teorema di Kruskal, esempi di wqo;
    4. applicazioni: protocolli di broadcast, canali con perdita di informazione, ecc;
    5. sistemi basati su array: format delle formule per le transizioni, per gli stati iniziali e finali;
    6. procedure di decisione negli algoritmi di 'backward reachability'.

  3. Orari delle lezioni

    4. L'orario di ricevimento del prof. Ghilardi è il venerdì mattina alle ore 11.30.

  4. Modalità d'esame

    5. L'esame sarà costitutito da un colloquio e da un progetto. È possibile sostituire (in tutto o in parte) gli argomenti del corso utilizzando materiale didattico che verrà fornito dal docente su richiesta.

  5. Materiali didattici

    6. Il corso viene tenuto per la prima volta; date le sue caratteristiche, il materiale didattico si baserà su appunti tratti dalle lezioni e dalle discussioni in aula. Indichiamo qui oltre però anche del materiale più strutturato che potrebbe risultare utile.

    1. Per la parte relativa alle procedure di decisione, indichiamo il testo di A. Bradley - Z. Manna "The Calculus of Computation (Decision Procedures with Applications to Verification)", Springer 2007.
    2. Per informazioni generali sul model checking a stati infiniti, indichiamo due articoli interessanti scaricabili qui e qui.

    La pagina web del sistema MCMT si trova qui. Da tale pagina si possono scaricare: (i) gli eseguibili per Linux e Mac (esiste anche una versione del sistema per Windows che verrà fornita direttamente dal docente su richiesta); (ii) il manuale utente e una serie di files di esempi già pronti; (iii) articoli vari relativi sia agli aspetti teorici che a quelli implementativi.

  6. Appelli d'esame

    7. L'esame è su appuntamento e può essere sostenuto (previo accordo con il docente) durante un qualsiasi orario di ricevimento. Per la registrazione formale, occorre iscriversi al SIFA al più una settimana prima, in corrispondenza delle date degli appelli del corso di Logica Matematica della Laurea Magistrale.

    Ultimo aggiornamento: 1/4/2010