Training and Research
PhD Programme Courses/classes
This page shows the PhD course's training activities for the academic year 2024/2025. Further activities will be added during the year. Please check regularly for updates!
Introduction to Blockchain
Credits: 3
Language: English
Teacher: Nicola Fausto Spoto
Principles and Applications of Abstract Interpretation
Credits: 3
Language: English
Teacher: Michele Pasqua
AI and explainable models
Credits: 5
Language: English
Teacher: Lorenza Brusini
Automated Software Testing
Credits: 4
Language: English
Teacher: Mariano Ceccato
Multi Omics Patient Stratification
Credits: 3
Language: English
Teacher: Rosalba Giugno
ACADEMIC WRITING IN LATEX
Credits: 3
Language: English
Teacher: Enrico Gregorio
A practical interdisciplinary PhD course on exploratory data analysis
Credits: 4
Language: English
Teacher: Rui Pedro Fernandes Ribeiro
Cyber-physical systems security
Credits: 3
Language: English
Teacher: Massimo Merro
Elements of Machine Learning
Credits: 3
Language: English
Teacher: Ferdinando Cicalese
Genomica informazionale: contenuto informativo dei genomi e s divergenza dalla randomicità
Credits: 3
Language: English
Introduction to Quantum Machine Learning
Credits: 3
Language: English
Teacher: Alessandra Di Pierro
Laboratory of quantum information in classical wave-optics analogy
Credits: 3
Language: English
Teacher: Claudia Daffara
Principles and Applications of Abstract Interpretation (2024/2025)
Teacher
Referent
Credits
3
Language
English
Class attendance
Free Choice
Location
VERONA
Learning objectives
Abstract Interpretation is a theory that deals with approximating mathematical structures, specifically those related to the semantic models of computer systems. It offers a systematic approach to constructing methods and effective algorithms for approximating undecidable or complex problems in computer science. A prominent example is program verification, where the correctness of a computer program is checked against a formal specification. Despite being an undecidable problem, Abstract Interpretation-based static analysis has been successful in automatically verifying the correctness of complex computer systems up to a given degree of approximation.
The course is meant to introduce the theory of Abstract Interpretation and to present its application to static analysis (the automatic, compile-time determination of semantic properties of programs) and program verification (conformance to a specification). The course also explores real-world examples of how Abstract Interpretation has been adopted in industry (e.g., by Meta).
Prerequisites and basic notions
Basic knowledge of programming languages and discrete mathematics.
Program
The course program includes the following topics:
- Foundations of Abstract Interpretation Theory
- Introduction to program verification by Abstract Interpretation
- Numerical analyses of imperative programs
- Tools to support automated program analysis and verification
Didactic methods
Frontal lectures.
Learning assessment procedures
Written assignment at the end of the course.
Assessment
Clarity, quality and completeness of the assignment.
Criteria for the composition of the final grade
Assignment evaluation.
Scheduled Lessons
| When | Classroom | Teacher | topics |
|---|---|---|---|
|
Tuesday 08 October 2024 12:30 - 15:30 Duration: 3:00 AM |
Ca' Vignal 1 - Auletta Atrio CV1 [T.H - terra] | Michele Pasqua | Introduction to the Abstract Interpretation and program verification. Mathematical background. |
|
Thursday 10 October 2024 09:30 - 12:30 Duration: 3:00 AM |
Ca' Vignal 2 - Riunioni (II piano) [15 - 2] | Michele Pasqua | Abstract Interpretation primer. Program semantics and fixpoint abstraction. |
|
Tuesday 15 October 2024 12:30 - 15:30 Duration: 3:00 AM |
Ca' Vignal 1 - Auletta Atrio CV1 [T.H - terra] | Michele Pasqua | Application of Abstract Interpretation to static analysis and program verification. Numerical abstractions. |
|
Thursday 17 October 2024 13:30 - 16:30 Duration: 3:00 AM |
Ca' Vignal 1 - Auletta Atrio CV1 [T.H - terra] | Michele Pasqua | Industrial adoption of Abstract Interpretation. Analysis of hyperproperties by Abstract Interpretation. |
