28789 - Program Analysis

Academic Year 2008/2009

  • Docente: Cosimo Laneve
  • Credits: 12
  • SSD: INF/01
  • Language: Italian
  • Teaching Mode: Traditional lectures
  • Campus: Bologna
  • Corso: Second cycle degree programme (LM) in Computer Science (cod. 8028)

Learning outcomes

At the end of the course, the student: - knows the main techniques for the analysis and the optimization of codes in compilers; - knows the techniques of static analysis with the abstract interpretation; - is able to estimate a technique a static analysis technique; - is able to propose a project for guaranteeing some program property.

Course contents

  • Introduction: the techniques for the program analysis.
  • Hoare logic: caso di studio su un semplice linguaggio imperativo.
  • Abstract interpretation: abstract domains, closures, widening, narrowing, interval analysis, constant propagation.
  • Data-flow analysis.
  • Techniques for the program analysis in the companies. 

Readings/Bibliography

  • K. Apt: Ten years of Hoare Logic: a survey", ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 3 ,  Issue 4  (October 1981), Pages: 431 - 483.
  • D. Volpano, G. Smith, C. Irvine: ``A sound type system for secure flow analysis'', Journal of Computer Security 1996. 
  • D. Volpano, G. Smith: ``A type-based approach to program security'', TAPSOFT'97. 
  • N. D. Jones, F. Nielson: ``Abstract interpretation, a semantic based tool for program analysis'', 1994 

Teaching methods

lectures.

Assessment methods

written or oral examination.

Teaching tools

projector.

Links to further information

http://www.cs.unibo.it/~laneve/programanalysis

Office hours

See the website of Cosimo Laneve