Abstract Interpretation

Contents

Can we guarantee that a program has no integer overflow? that there is no buffer over-run, no null-pointer is dereferenced and all accesses to arrays are within the array bounds? Abstract Interpretation (AI, for short) is a general technique to automatically infer certificates in that respective or hint at suspicious places in the code.

This hands-on class introduces into basic concepts and techniques of Abstract Interpretation as well as advanced constructions and recent developments in the field.
Lectures with be intertwined with exercises where participants will be able to solve problems on their own. Bonus points will be received for developping a static analyzer in a language of their liking.

Organisation

This winter semester the lectures and tutorials take place in person.

All information about the course will be available on Moodle. Throughout the semester all announcements will be communicated via Moodle as well.

There will be assignments that we will discuss and interactively solve during the tutorial sessions. 

The tutorial is given by Helmut Seidl.

Bibliography

• Helmut Seidl, Reinhard Wilhelm and Sebastian Hack. Compiler Design - Analysis and Transformation. Springer, 2012.
• Helmut Seidl, Reinhard Wilhelm and Sebastian Hack. Übersetzerbau 3: Analyse und Transformation. Springer, 2010.