Practicalities

Time: February 2-6 (Monday-Friday), 2015
Place: Business-center "Times", 4th floor,
Kantemirovskaya street, 2-А,
197342, Saint Petersburg, Russia
Registration: Free (contact Dmitri Boulytchev <> to register)
Organizer: JetBrains' Programming Languages and Tools Lab at SPbSU

Description

The winter school provides a basic introduction to abstract interpretation. In the classical framework the execution of programs is modelled by a transition system. The space of possible program executions (the collecting semantics) is then systematically over-approximated through Galois connections. We will study both the theoretical, mathematical foundation, as well as implement the resulting analyses in practice as executable abstract interpreters.

Lecturer

Jan Midtgaard <>

Please do not hesitate to contact me in case of comments or questions regarding the winter school.

Practicalities

The course will consist of both lectures (generally: mornings), theoretical exercises, and practical exercises (generally: afternoons). Participants should therefore bring their computer.

Schedule (subject to rearrangements)

Lecture Topic Course Material Exercises
Mon
Feb 2
Course intro +
Basic concepts of abstract interpretation +
OCaml intro
Slides day 1
transsys.ml
Cousot-Cousot:BIS04
Exercises day 1
Tue
Feb 3
Operational semantics +
Calculating an analysis I
Slides day 2
alphagammagym.txt
Plotkin:TR81,chap.1
3CounterMach
Optional:
Danvy:3steps, Flanagan-al:PLDI93
Siveroni:JLAP04, Ager-al:PPDP03
Exercises day 2
Wed
Feb 4
Concepts of abstract interpretation +
Calculating an analysis II
Slides day 3
alphagammagym2.txt
Cousot-Cousot:JLP92, p.1-18 (Sec.7-10 optional) Cousot-Cousot:POPL79 (optional)
Exercises day 3
Thu
Feb 5
More concepts of abstract interpretation +
Numerical and structural abstractions
Slides day 4
Cousot-Cousot:JLP92, p.18-39 (Sec.7-10 optional)
Miné:thesis,Sec. 2.4.5 - 2.5
Deutsch:POPL90
Cousot-Cousot:ISOP76 (optional)
Cousot-Cousot:POPL77 (optional)
Cousot-Cousot:JLC92, (optional)
Cousot-Cousot:ICCL94 (optional treasure chest of Galois connections)
Exercises day 4
Fri
Feb 6
Case studies:
Abstract debugging + Astrée
QuickChecking static analysis properties
Slides day 5
Miné's PLDI'93 slides
Quickchecking slides
Bourdoncle:PLDI93
Blanchet-al:PLDI03
LCheck
Exercises day 5

Links to supplementary material

OCaml resources

Abstract Interpretation links

Tools based on Abstract Interpretation

Paper links (approaching propaganda)

Similar courses elsewhere