UP | HOME
a_software.gif
tercer_nivel_software.gif

UPM / IMDEA Track in Software Development through Rigorous Methods

Abstract interpretation

Coordinator(s)/Instructor(s)

Length

4 credits (ECTS)

Prerequisites

Abstract interpretation is a formal mathematical framework. Therefore, students are expected to understand basic mathematical notations and set theory. In addition, practical sessions will be given, based on the Ocaml language. Students should already be familiar with a functional language and the yacc parser. Knowledge of compiler technology can help for this course.

This course has specific requirements, and if your initial level is not adequate, you may not pass. Therefore, we ask you to please include it in the mail you ought to send to graduate.school (at) software.imdea.org with the list of courses you want to take from the IMDEA track. You will receive a mail stating the courses in which you are welcome to enroll. If you enroll in an IMDEA Track course for which you did not receive explicit approval, you may be asked to switch over to a different one.

Course web page (if any)

Not yet available.

Summary and objectives

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.

The objective of the course will be to give the basics of abstract interpretation, and to describe some applications.

Topics

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

Evaluation

Students will be evaluated based on a presentation of their practical work.

Recommended reading

Will be given based on the level of the students.



Back to the initial page
Go to the IMDEA Software Institute page

Fractals are used with permission from their author Cory Ench | © 2006-2007. IMDEA Software.
All rights reserved | Legal Notice | Privacy Policy