Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
VERIFICA DEL SOFTWARE
SCP6076339, A.A. 2018/19

Informazioni valide per gli studenti immatricolati nell'A.A. 2018/19

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2018/19
N0
porta questa
pagina con te
Crediti formativi 6.0
Tipo di valutazione Voto
Denominazione inglese SOFTWARE VERIFICATION
Sito della struttura didattica http://informatica.scienze.unipd.it/2018/laurea_magistrale
Dipartimento di riferimento Dipartimento di Matematica
Obbligo di frequenza No
Lingua di erogazione ITALIANO
Sede PADOVA
Corso singolo È possibile iscriversi all'insegnamento come corso singolo
Corso a libera scelta È possibile utilizzare l'insegnamento come corso a libera scelta

Docenti
Responsabile FRANCESCO RANZATO INF/01

Dettaglio crediti formativi
Tipologia Ambito Disciplinare Settore Scientifico-Disciplinare Crediti
CARATTERIZZANTE Discipline Informatiche INF/01 6.0

Organizzazione dell'insegnamento
Periodo di erogazione Primo semestre
Anno di corso I Anno
Modalità di erogazione frontale

Tipo ore Crediti Ore di
didattica
assistita
Ore Studio
Individuale
LEZIONE 6.0 48 102.0

Calendario
Inizio attività didattiche 01/10/2018
Fine attività didattiche 18/01/2019
Visualizza il calendario delle lezioni Lezioni 2019/20 Ord.2014

Commissioni d'esame
Commissione Dal Al Membri
3 a.a. 2018/2019 01/10/2018 28/02/2020 RANZATO FRANCESCO (Presidente)
FILE' GILBERTO (Membro Effettivo)
CRAFA SILVIA (Supplente)
GAGGI OMBRETTA (Supplente)
SPERDUTI ALESSANDRO (Supplente)

Syllabus
Prerequisiti: Conoscenze di base dei linguaggi di programmazione. L'insegnamento non prevede propedeuticità.
Conoscenze e abilita' da acquisire: Il corso mira ad introdurre metodi e strumenti per la specifica del comportamento, l'analisi statica e la verifica automatica dei programmi e, più in generale, dei sistemi software. In particolare, il corso fornisce una introduzione alla semantica formale dei linguaggi di programmazione ed ai metodi formali per la loro analisi statica e verifica.
Modalita' di esame: Esame orale e/o progetto software, possibilmente suddivisi in parti distinte.
Criteri di valutazione: L'esame orale verte su vari esercizi che lo studente deve svolgere in modo indipendente a casa. Il progetto di laboratorio verte su qualche tool di verifica del software.
Contenuti: - Semantica dei programmi: Modellazione del comportamento (in particolare il comportamento input/output) dei programmi mediante la teoria dell'ordinamento e dei punti fissi. (cf. https://en.wikipedia.org/wiki/Semantics_(computer_science) )

- Analisi statica e verifica di programmi mediante interpretazione astratta: L'interpretazione astratta è una notoria tecnica basata su una approssimazione della semantica dei programmi che permette di specificare le proprietà dei programmi deducibili mediante analisi statica e di provarne la correttezza. (cf. https://en.wikipedia.org/wiki/Abstract_interpretation )

- Analisi statica dataflow di programmi: tecnica per dedurre staticamente informazioni sull'insieme dei possibili valori delle variabili nei vari punti del programma. Un grafo di flusso del controllo è utilizzato per determinare le parti di un programma a cui un particolare valore assegnato ad una variabile potrebbe propagarsi. Le informazioni raccolte sono spesso utilizzate dai compilatori (come gcc e javac) per ottimizzare un programma. (cf. https://en.wikipedia.org/wiki/Data-flow_analysis )

- Strumenti di verifica del software: ad esempio, Clousot (Microsoft, USA), Interproc (INRIA, Francia), Jandom (Università di Pescara) (cf. https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis )
Attivita' di apprendimento previste e metodologie di insegnamento: L'insegnamento prevede lezioni frontali e la risoluzione in modo indipendente a casa di vari esercizi e/o lo sviluppo di un progetto di verifica del software.
Eventuali indicazioni sui materiali di studio: Le slide utilizzate a lezione verranno distribuite.
Testi di riferimento:
  • H. Riis Nielson, F. Nielson, Semantics with Applications: A Formal Introduction. --: Wiley, 1992. Electronic version freely available
  • Antoine Minè, Tutorial on static inference of numeric invariants by abstract interpretation. --: Now, The Essence of Knowledge, 2017. Journal: Foundations and Trends in Programming Languages

Didattica innovativa: Strategie di insegnamento e apprendimento previste
  • Lecturing
  • Laboratory
  • Problem based learning
  • Case study
  • Interactive lecturing
  • Working in group
  • Questioning
  • Problem solving
  • Files e pagine caricati online (pagine web, Moodle, ...)

Didattica innovativa: Software o applicazioni utilizzati
  • Moodle (files, quiz, workshop, ...)

Obiettivi Agenda 2030 per lo sviluppo sostenibile
Istruzione di qualita' Uguaglianza di genere