SOFTWARE AND SYSTEM VERIFICATION-2

Academic year
2024/2025 Syllabus of previous years
Official course title
SOFTWARE AND SYSTEM VERIFICATION-2
Course code
PHD207-2 (AF:545152 AR:311536)
Modality
On campus classes
ECTS credits
2
Degree level
Corso di Dottorato (D.M.226/2021)
Educational sector code
INF/01
Period
Annual
Course year
1
Where
VENEZIA
Moodle
Go to Moodle page
The goal of this course is to teach the main concepts of the abstract interpretation theory and its application and implementation to some common contexts (in particular, about numerical and heap abstractions).
At the end of the course, the student will be able to:
1) understand the main institutions, certifications, and standards in the field of quality and security assurance
2) understand the formalization and proof of soundness of abstract interpretation-based static analyses
3) implement some basic analyses in a generic static analyzer based on the abstract interpretation theory.
Basic knowledge of algebra. Knowledge of the Java programming language.
1) Introduction to static program analysis
2) Software quality assurance
3) Bases of abstract interpretation
4) Numerical domains
5) Heap abstraction
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 )
Implementation of some analyses in a generic static analyzer or presentation of a scientific paper on abstract interpretation.
oral
Frontal lectures, slides, and live coding.
English
Definitive programme.
Last update of the programme: 18/09/2024