Il corso presenterà i metodi e gli strumenti per specificare ed analizzare modelli di sistemi basati sul software e le loro implementazione. Presenterà la letteratura fondamentale riguardo a:

• Linguaggi per esprimere modelli di sistemi basati sul software;
• Linguaggi per esprimere le proprietà di interesse dei modelli e delle loro implementazioni software;
• Algoritmi per decidere se un modello o una implementazione software ha una determinata proprietà di interesse.

Il corso sarà basato su un insieme di strumenti software disponibili per l'uso accademico. La teoria sarà alternata con un insieme di sessioni di esercitazioni pratiche basate su esempi rilevanti, che permetteranno agli studenti di acquistare confidenza con gli strumenti software per l'analisi dei modelli e dei programmi presentati nel corso.

Argomenti:

1. Analisi del software 1: esecuzione simbolica (Braione)
2. Analisi del software 2: analisi dataflow (Denaro)
   
3. Specifica e analisi dei modelli 1: modelli relazionali (Braione)
4. Specifica e analisi dei modelli 2: model checking (Denaro)
   
5. Argomento da decidere con gli studenti (analisi del software 3 oppure specifica e analisi dei modelli 3) (Braione)