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:526020 AR:296114)
Modality
On campus classes
ECTS credits
2
Degree level
Corso di Dottorato (D.M.45)
Educational sector code
INF/01
Period
Annual
Course year
1
Where
VENEZIA
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 about algebra.
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 value analyses in a generic static analyzer and discussion about the adopted implementation.
Frontal lectures and slides.
English
oral
Definitive programme.
Last update of the programme: 06/03/2024