concrete program analysis techniques, proof of the correctness of these techniques via abstract interpretation, techniques for developing new program analyses
definition of the syntax and semantics of a toy programming language;
simple program analyses, which are used standardly in compilers, such as Reaching Definitions, Live Variable Analysis and Constant Propagation;
program analyses, which are used in program verification such as Interval-, Octagon-, Polyederanalysis for determining program invariants;
advanced program analyses, which are used standardly in compilers, such as Pointer Analysis and Call Graph Analysis;
advanced topics in invariant analysis such as termination- and bound analysis;
the discussed program analyses are defined and proven correct with the technique of abstract interpretation with regard to the earlier defined toy language;
For further reading I recommond:
Static Analylsis Course and Script by Michael Schwartzbach, http://cs.au.dk/~mis/static/
Course on Abstract Interpretation by Patrick Cousot, http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/
The Book Principles of Program Analysis by Flemming Nielson, Hanne Riis Nielson, Chris Hankin
The participants of this lecture give a talk and write a report on a current paper on program analysis. List of presentation topics:
Precise interprocedural dataflow analysis via graph reacability, Reps, Horwitz, and Sagiv, 1995
Points-to analysis with efficient strong updates, Lhotak, Chung, 2011
Semi-sparse flow-sensitive pointer analysis, Hardekopf, Lin, 2009
Parametric shape analysis via 3-valued logic, Sagiv, Reps, Wilhelm, 2002
A parametric segmentation functor for fully automatic and scalable array content analysis, Cousot, Cousot, Logozzo, 2011
Forest automata for verification of heap manipulation, Habermehl, Holík, Rogalwicz, Ji¿í Šimá¿ek und Tomáš Vojnar, 2011
Verification of parameterized concurrent programs by modular reasoning about data and control, Farzan, Kincaid, 2012
Improving strategies via SMT solving, Gawlitza, Monniaux, 2011
Precise interprocedural analysis through linear algebra, Müller-Olm, Seidl, 2004
The octagon abstract domain, Miné, 2006
Combining abstract interpreters, Gulwani, Tiwari, 2006
