SOFTWARE AND SYSTEM VERIFICATION-2

Anno accademico
2024/2025 Programmi anni precedenti
Titolo corso in inglese
SOFTWARE AND SYSTEM VERIFICATION-2
Codice insegnamento
PHD207-2 (AF:545152 AR:311536)
Modalità
In presenza
Crediti formativi universitari
2
Livello laurea
Corso di Dottorato (D.M.226/2021)
Settore scientifico disciplinare
INF/01
Periodo
Annuale
Anno corso
1
Sede
VENEZIA
Spazio Moodle
Link allo spazio del corso
L'obiettivo di questo corso è insegnare i concetti principali della teoria dell'interpretazione astratta e la sua applicazione e implementazione ad alcuni contesti comuni (in particolare, riguardo alle astrazioni numeriche e dello heap).
Al termine del corso, lo studente sarà in grado di:
1) comprendere le principali istituzioni, certificazioni e standard nel campo della garanzia della qualità e della sicurezza
2) comprendere la formalizzazione e la prova di solidità di analisi statiche basate sull'interpretazione astratta
3) implementare alcune analisi di base in un generico analizzatore statico basato sulla teoria dell'interpretazione astratta.
Conoscenze di base di algebra. Conoscenze del linguaggio di programmazione Java.
1) Introduzione all'analisi statica di programma
2) Garanzia della qualità del software
3) Basi di interpretazione astratta
4) Domini numerici
5) Astrazione dell'heap
Xavier Rival and Kwangkeun Yi: "Introduction to Static Analysis: An Abstract Interpretation Perspective", MIT Press, 2019 (https://mitpress.mit.edu/books/introduction-static-analysis )
Patrick Cousot: "Principles of Abstract Interpretation", MIT Press, 2021 (https://mitpress.mit.edu/books/principles-abstract-interpretation )
Implementazione di alcune analisi in un analizzatore statico generico o presentazione di un articolo scientifico sull'interpretazione astratta.
Lezioni frontali, slides, e live coding.
Inglese
orale
Programma definitivo.
Data ultima modifica programma: 18/09/2024