Master in Software and Systems

Abstract Interpretation

Lecturer (Coordinator):
Manuel Carro
mcarro@fi.upm.es
Lecturer:
Pierre Ganty
pierre.ganty@imdea.org

Semester

Second semester

Credits

4 ECTS

Outline

Abstract interpretation is a formal mathematical framework which makes it possible to define and implement program analyses which are correct by construction -- provided that some basic properties are met. Software is an essential part of more and more complex systems. In order to master that complexity, it is necessary to be able to compute automatically reliable information about software. This is the goal of static analysis. To reason rigorously about programs, mathematical models of the behavior or programs are developed. Such models are called semantics. Depending on the properties to compute, we can use different semantics - some more detailed for more precision, others coarser for more efficiency. Abstract interpretation is a theory of approximation that allows the comparison of different semantics, or building new semantics through refinement or abstraction. Because all interesting properties of programs are undecidable, all static analysis methods introduce approximations in one way or another. Therefore, abstract interpretation is a good framework to give a unified vision of such methods and to compare them.

Learning Goals

Syllabus

  1. An informal introduction
  2. Program properties
  3. Property approximations
  4. Morphisms and connections
  5. Abstraction of fixpoints
  6. Conception of a reachability analysis
  7. Applications
  8. Approximated fixpoints and widening
  9. Refinement of analyses

Website

http://www.software.imdea.org/graduateschool

Prerequisites

Assessment Method

Tuition Language

English

Subject-Specific Competences

More information:

This table shows the code, description and proficiency level for each subject-specific competence

Code Competence Proficiency Level
SSC1 Examination of the state of the art to identify research problems related to the design, construction, use and evaluation of complex software-intensive sociotechnical systems S
SSC5 Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools A

Learning Outcomes

More information:

This table shows the code, description and proficiency level for each subject learning outcome

Code Learning Outcome Associated competences Proficiency level
RA-AV-8 Ability to use existing program static analysis, program formal verification and automatic program transformation tools SSC5 A
RA-AV-9 Knowledge of the foundations of abstract interpretation as a method of program static analysis SSC1 K

Learning Guide

Subject learning guide for Abstract Interpretation