Corso di laurea in Informatica

Sono richieste conoscenze elementari di logica e buone conoscenze di programmazione e algoritmi; inoltre si assume che lo studente possegga nozioni di linguaggi formali.
Insegnamenti propedeutici (forniscono le competenze attese in ingresso): Matematica Discreta e Logica, Programmazione 1 e 2, Algoritmi e Strutture Dati, Linguaggi Formali e Traduttori.

L'insegnamento si propone di offrire agli studenti le conoscenze di base relative all'analisi ed alla verifica formale di proprietà dei programmi. Gli obiettivi dell'insegnamento dei metodi formali fanno parte degli Obiettivi formativi specifici del CdS in Informatica (L31), in particolare sono tra quelli relativi all'area di approfondimento dell'informatica. A questo scopo vengono introdotte le basi teoriche della modellazione e dell'analisi statica del comportamento dei programmi. Quindi sarà trattato un semplice linguaggio imperativo, di cui verranno esposti la semantica operazionale e quella logica, basata sulla logica di Hoare. Infine si utilizzeranno alcuni tools per la sperimentazione pratica delle metodologie trattate.

CONOSCENZA E CAPACITÀ DI COMPRENSIONE Acquisizione della conoscenza di alcune tecniche per la verifica formale della correttezza funzionale di programmi basate sulla logica e sulla specifica mediante "contratti".

CAPACITÀ DI APPLICARE CONOSCENZA E COMPRENSIONE Acquisizione della capacità di costruire dimostrazioni formali di correttezza dei programmi mediante l'uso di un tool, ed in particolare di proof-assistant.

AUTONOMIA DI GIUDIZIO Acquisizione di consapevole autonomia di giudizio con riferimento alla valutazione alla necessità di sviluppare il codice dei programmi in modo ben strutturato e di documentarlo in modo formalmente preciso per facilitarne la verifica ed assicurarne l'affidabilità.

ABILITÀ COMUNICATIVE Acquisizione di competenze e strumenti per la comunicazione nella forma scritta e orale per documentare la correttezza ed affidabilità dei programmi o al contrario per evidenziarne i punti deboli.

CAPACITÀ DI APPRENDIMENTO Acquisizione di capacità autonome di apprendimento e di autovalutazione della propria preparazione, atte ad intraprendere gli studi successivi con un alto grado di autonomia.

 

• Metodi formali
  • Automi e program graphs
  • Comandi con guardie
  • Verifica di programmi
  • Analisi statica
  • Language based security
  • Model checking
• Fondamenti di linguaggi di programmazione procedurali
  
  • Semantica operazionale big-step e small-step
  • Sistemi di tipo per IMP
  • Tipi per la sicurezza
  • Logica di Hoare
  • Verification conditions
• Verifica funzionale di programmi imperativi ed object-oriented
  • Specifica con asserzioni
  • Loop ed invarianti
  • Tipi di dato induttivi
  • Tipi di dato astratto e moduli
  • Specifica e verifica di oggetti e classi

Le lezioni si svolgeranno in presenza e verranno registrate. Le registrazioni, il testo, i lucidi, le dispense ed altro materiale didattico saranno forniti attraverso la pagina Moodle dell'insegnamento.

L'esame consiste in un colloquio orale in cui, oltre agli argomenti della teoria indicati nel programma, verranno discusse le consegne effettuate attraverso la piattaforma Moodle in itinere o, per i non frequentanti, almeno una settimana prima dell'appello.