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.
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 |
The course will consist of both lectures (generally: mornings), theoretical exercises, and practical exercises (generally: afternoons). Participants should therefore bring their computer.
Lecturer
Please do not hesitate to contact me in case of comments or questions regarding the winter school.
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
- Tutorial and toplevel in your browser
- A nice OCaml community site
- The OCaml homepage at INRIA
- The OCaml reference manual
- The OCaml standard library API
- Jason Hickey's OCaml book
Abstract Interpretation links
- Wikipedia's entry on Abstract Interpretation
- PPL - the Parma Polyhedra Library
- APRON - numerical abstract domain library
Tools based on Abstract Interpretation
- The ASTRÉE Static Analyzer, available as a product from AbsInt.com
- Mathworks's Polyspace verifiers
- ECLAIR from BUGSENG
- CodeHawk from Kestrel Technologies
- SPARROW from Fasoo
Paper links (approaching propaganda)
- Model-checking as abstract interpretation
- Parsing as abstract interpreation
- Proof-carrying code by (certified) abstract interpretation
- Types as abstract interpretation
- Static analysis of obfuscated x86 binaries by abstract interpretation
Similar courses elsewhere
- Patrick Cousot's Abstract Interpretation course at MIT
- Giorgio Levi's Abstract Interpretation course at Università di Pisa
- Fred Mesnard's Abstract Interpretation course at Université de la Reunion
- Xavier Rival's Static analysis course at École Polytechnique (in French)