The first part of the course, focusing on compilers, is taught by
Christophe Alias. You find below material for the second part of the
course, about program analysis and related topics.
TP and TD: here
and here (go
figure).
Program analysis
Catch up course
slides - Caml
code
Additional reference:
for Hoare logic, see chapter 6 of Glynn Winskel's book "The
Formal Semantics of Programming Languages" (available at the
library)
Abstract Interpretation
slides for the
lecture (most of it is on the blackboard, though);
(printable version).
demo files (kindly provided by P.Roux and
A.Miné)
Additional references:
online
course (concentrate on the first lectures, given by Antoine Miné)
online
material by Pierre Roux (whom we thank for his help in preparing
the TP), including an application to flowers
Hoare triples and separation logic
slides for the
lecture (printable
version) --- again, most of it is on the blackboard.
Additional references:
course
notes by Peter O'Hearn.
Sections 1 to 3 are the most relevant
for the course.
tutorial
paper by John Reynolds
A lot of material there, you can use it to check for the precise
definition of something we discussed in the course.
Executing and Compiling Functional Languages
slides for the
lectures,
(printable version)
the flawedinterpreter for
the semantics with environments (compile it by running make,
then run ./main.native)
files for the lecture about program transformations
(the slides of that lecture are available above)
Additional references: