UPM / IMDEA Software Institute Specialization Track in Software Development through Rigorous Methods (2017-2018)
Table of Contents
Note: this course is taught at the the IMDEA Software Institute (in the Montegancedo Campus, 500 m. from the CS School). Please get in touch with the coordinator or one of the instructors for more details regarding the exact meeting place and possible schedule changes.
This course has specific requirements. If you are not a student affiliated to the IMDEA Software Institute, please follow these instructions. If you do not follow them, you may be asked to register in some other course.
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.
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
- An informal introduction
- Program properties
- Property approximations
- Morphisms and connections
- Abstraction of fixpoints
- Building a reachability analysis
- Applications
- Approximated fixpoints and widening
- 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
