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:526020 AR:296114)
Modalità
In presenza
Crediti formativi universitari
2
Livello laurea
Corso di Dottorato (D.M.45)
Settore scientifico disciplinare
INF/01
Periodo
Annuale
Anno corso
1
Sede
VENEZIA
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.
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 dei valori in un analizzatore statico generico e discussione dell'implementazione adottata.
Lezioni frontali e slides.
Inglese
orale
Programma definitivo.
Data ultima modifica programma: 06/03/2024