SOFTWARE CORRECTNESS, SECURITY, AND RELIABILITY

Anno accademico

2026/2027 Programmi anni precedenti

Titolo corso in inglese

SOFTWARE CORRECTNESS, SECURITY, AND RELIABILITY

Codice insegnamento

CM0476 (AF:733825 AR:436306)

Lingua di insegnamento

Inglese

Modalità

In presenza

Crediti formativi universitari

6

Livello laurea

Laurea magistrale (DM270)

Settore scientifico disciplinare

INFO-01/A

Periodo

II Semestre

Anno corso

1

Sede

VENEZIA

Inquadramento dell'insegnamento nel percorso del corso di studio

Questo insegnamento appartiene al percorso Security del corso di laurea magistrale in Computer Science, ed offre contenuti e metodologie relative metodi e strumenti per la verifica del software.

Risultati di apprendimento attesi

L'obiettivo dell'isegnamento è formire una panoramica delle principali tecniche per l'analisi e la verifica di codice sorgente. L'affidabilità del software dipende fortemente dalla correttezza delle sue componenti. Il corso sottiolinea i vantaggi ed i limiti delle tecniche di analisi statica rispetto alle tecniche di testing, e discute le metriche e gli standards per l'assicurazione di qualità dei prodotti software. Al termine del corso gli studenti saranno in grado di utilizzare e di estendere un analizzatore statico per la verifica di codice sorgente.

Prerequisiti

Strutture Algebriche di base, Linguaggi di Programmazione

Contenuti

1. Semantics-based techniques for correctness and security analysis
Trace Semantics and Fixpoints
Dataflow Analysis
Abstract Interpretation
Numerical and String domains for source code verification

2. Software Quality Assurance
Software quality metrics
Software quality standards
Software quality management
Software Safety and Reliability

Testi di riferimento

Xavier Rival and Kwangkeun Yi, "Introduction to Static Analysis An Abstract Interpretation Perspective", MIT Press, 2020, ISBN: 9780262043410
G.Schulmeyer, “Handbook of Software Quality Assurance”, 2007, ISBN-13: 978-1596931862
P.Cousot, "Principles of Abstract Interpretation, MIT Press, 2021

Modalità di verifica dell'apprendimento

Ogni settimana verrà assegnato un task che via via accompagnerà lo studente all'utilizzo di un analizzatore statico a livello professionale.
L'esame finale consisterà nella discussione di un progetto finale (che potrà essere svolto anche in coppia), in continuità con i task individuali svolti durante il corso.

Modalità di esame

orale

Il/la docente ha il dovere di vigilare affinché siano rispettate le regole di autenticità e originalità delle prove d'esame. Di conseguenza, nei casi in cui vi sia il sospetto di un comportamento irregolare, l'esame può prevedere un ulteriore approfondimento, contestuale alla prova d'esame, che potrà essere realizzato anche in modalità differente rispetto alle modalità sopra riportate.

Graduazione dei voti

Ciascun task avrà una valutazione (in decimi) in base al numero di test superati.
La valutazione finale terrà conto per un 30% della valutazione media dei task e per il 70% della correttezza e della completezza del progetto realizzato e della relativa documentazione.

Metodi didattici

Lezioni frontali, lavori di gruppo, revisione degli esercizi proposti
Tutto il materiale didattico sarà messo a disposizione sulla piattaforma Moodle.

Obiettivi Agenda 2030 per lo sviluppo sostenibile

Questo insegnamento tratta argomenti connessi alla macroarea "Capitale umano, salute, educazione" e concorre alla realizzazione dei relativi obiettivi ONU dell'Agenda 2030 per lo Sviluppo Sostenibile

Programma definitivo.

Data ultima modifica programma: 04/04/2026