Training and Research

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.

Students with disabilities or specific learning disorders (SLD), who intend to request the adaptation of the exam, must follow the instructions given HERE

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 Abstract Interpretation and 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 and program semantics.
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.
Thursday 17 October 2024
13:30 - 16:30
Duration: 3:00 AM
Ca' Vignal 1 - Auletta Atrio CV1 [T.H - terra] Michele Pasqua Numerical abstractions and industrial adoption of Abstract Interpretation.

PhD school courses/classes - 2024/2025

Please note: Additional information will be added during the year. Currently missing information is labelled as “TBD” (i.e. To Be Determined).

1. PhD students must obtain a specified number of CFUs each year by attending teaching activities offered by the PhD School.
First and second year students must obtain 8 CFUs. Teaching activities ex DM 226/2021 provide 5 CFUs; free choice activities provide 3 CFUs.
Third year students must obtain 4 CFUs. Teaching activities ex DM 226/2021 provide 2 CFUs; free choice activities provide 2 CFUs.
More information regarding CFUs is found in the Handbook for PhD Students: https://www.univr.it/phd-vademecum

2. Registering for the courses is not required unless explicitly indicated; please consult the course information to verify whether registration is required or not. When registration is actually required, instructions will be sent well in advance. No confirmation e-mail will be sent after signing up. Please do not enquiry: if you entered the requested information, then registration was silently successful.

3. When Zoom links are not explicitly indicated, courses are delivered in presence only.

4. All information we have is published here. Please do not enquiry for missing information or Zoom links: if the information you need is not there, then it means that we don't have it yet. As soon as we get new information, we will promptly publish it on this page.

Summary of training activities

Teaching Activities ex DM 226/2021: Linguistic Activities

Teaching Activities ex DM 226/2021: Research management and Enhancement

Teaching Activities ex DM 226/2021: Statistics and Computer Sciences

Teaching Activities: Free choice

Faculty

B C D F G L M O P Q R S V

Belussi Alberto

symbol email alberto.belussi@univr.it symbol phone-number +39 045 802 7980

Bicego Manuele

symbol email manuele.bicego@univr.it symbol phone-number +39 045 802 7072

Bonacina Maria Paola

symbol email mariapaola.bonacina@univr.it symbol phone-number +39 045 802 7046

Brusini Lorenza

symbol email lorenza.brusini@univr.it symbol phone-number +39 045 802 7874

Carra Damiano

symbol email damiano.carra@univr.it symbol phone-number +39 045 802 7059

Castellani Umberto

symbol email umberto.castellani@univr.it symbol phone-number +39 045 802 7988

Castellini Alberto

symbol email alberto.castellini@univr.it symbol phone-number +39 045 802 7908

Ceccato Mariano

symbol email mariano.ceccato@univr.it

Cicalese Ferdinando

symbol email ferdinando.cicalese@univr.it symbol phone-number +39 045 802 7969

Combi Carlo

symbol email carlo.combi@univr.it symbol phone-number +39 045 802 7985

Cristani Matteo

symbol email matteo.cristani@univr.it symbol phone-number +39 045 802 7983

Daducci Alessandro

symbol email alessandro.daducci@univr.it symbol phone-number +39 045 802 7025

Daffara Claudia

symbol email claudia.daffara@univr.it symbol phone-number +39 045 802 7942

Dalla Preda Mila

symbol email mila.dallapreda@univr.it

Di Pierro Alessandra

symbol email alessandra.dipierro@univr.it symbol phone-number +39 045 802 7971

Farinelli Alessandro

symbol email alessandro.farinelli@univr.it symbol phone-number +39 045 802 7842

Fernandes Ribeiro Rui Pedro

symbol email rui.ribeiro@univr.it symbol phone-number 0458027905

Giugno Rosalba

symbol email rosalba.giugno@univr.it symbol phone-number +39 045 802 7066

Gregorio Enrico

symbol email Enrico.Gregorio@univr.it symbol phone-number +39 045 802 7937

Lissandrini Matteo

symbol email matteo.lissandrini@univr.it symbol phone-number +39 045802 8853

Mastroeni Isabella

symbol email isabella.mastroeni@univr.it symbol phone-number +39 045 802 7089

Merro Massimo

symbol email massimo.merro@univr.it symbol phone-number +39 045 802 7992

Migliorini Sara

symbol email sara.migliorini@univr.it symbol phone-number +39 045 802 7908

Oliboni Barbara

symbol email barbara.oliboni@univr.it symbol phone-number +39 045 802 7077

Paci Federica Maria Francesca

symbol email federicamariafrancesca.paci@univr.it symbol phone-number +39 045 802 7909

Pasqua Michele

symbol email michele.pasqua@univr.it

Posenato Roberto

symbol email roberto.posenato@univr.it symbol phone-number +39 045 802 7967

Quaglia Davide

symbol email davide.quaglia@univr.it symbol phone-number +39 045 802 7811

Quintarelli Elisa

symbol email elisa.quintarelli@univr.it symbol phone-number +39 045 802 7852

Rospocher Marco

symbol email marco.rospocher@univr.it symbol phone-number +39 045802 8326

Sala Pietro

symbol email pietro.sala@univr.it symbol phone-number +39 045 802 7850

Spoto Nicola Fausto

symbol email fausto.spoto@univr.it symbol phone-number +39 045 802 7940

Villa Tiziano

symbol email tiziano.villa@univr.it symbol phone-number +39 045 802 7034
Course lessons
PhD Schools lessons

Loading...

Guidelines for PhD students

Below you will find the files that contain the Guidelines for PhD students and rules for the acquisition of ECTS credits (in Italian: "CFU") for the Academic Year 2023/2024.

Documents

Title Info File
File pdf Dottorandi: linee guida generali (2023/2024) pdf, it, 93 KB, 26/02/24
File pdf PhD students: general guidelines (2023/2024) pdf, en, 94 KB, 26/02/24