Il Corso si terrà nel secondo semestre.
È stato aperto un sito sulla piattaforma Ariel all'indirizzo raggiungibile da qui. Il sito verrà man mano aggiornato nei tempi dovuti e conterrà dispense, notizie, link a strumenti software e materiale aggiuntivo.
Quest'anno il corso verrà erogato in presenza, con streaming tramite la piattaforma Microsoft Teams. Gli studenti potranno accedere allo streaming utilizzando il codice che verà segnalato sulla piattaforma Ariel, nella sezione "Bacheca". La frequenza fisica è altamente consigliata, anche e soprattutto in vista delle attività di laboratorio. Agli studenti non frequentanti sarà richiesta la consegna di due progetti per accedere all'orale.
Chiedo agli studenti interessati al corso di mandarmi una email all'indirizzo silvio.ghilardi@unimi.it, in modo da poter costruire una lista dei frequentanti.
Il corso si propone di sviluppare le principali tecniche di ragionamento automatico, basate sia su metodi di saturazione e completamento, che su metodi di backtracking. Lo studente verrà introdotto all'utilizzo di alcuni strumenti quali superposition provers, SAT- e SMT-solvers, model finders, model-checkers. Sono previsti sbocchi applicativi sia verso l'algebra computazionale che verso la verifica di sistemi informatici.
L'orario di ricevimento del prof. Ghilardi è il venerdì mattina alle ore 11.00.
L'esame sarà costituito da un colloquio. La parte di laboratorio sarà coperta dalla semplice partecipazione attiva alle lezioni per gli studenti frequentanti; agli altri sarà assegnato un progetto. Sarà possibile concordare in tutto o in parte un programma specifico a fronte di esigenze particolari.
Si veda il sito Ariel sopra citato.
Secondo il calendario ufficiale degli appelli, con iscrizione al SIFA.