INF9906 - Selected topics in static analysis

Schedule, syllabus and examination date

Choose semester

Course content

Programming errors are, depending on the application, annoying till intolerable. Many theoretical methods have been developed to prove the correctness of programs. However, in practice the effort to verify realistic programs is immense, or often even unmanagable, so these methods are applied only in the most safety-critical applications and/or in special areas, for instance, hardware verification. To routinely eliminate errors in industrial programs, in contrast, only methods which identify a wide range of often encountered program errors efficiently and automatically, are acceptable.

Static analysis is a generic term for many such approaches. Examples of such approaches are

  • identify type inconsistencies by type checking,
  • potential nil-pointer derefencing,
  • security checks when downloading Java-applets,
  • estimations of communication overhead, and
  • resource bound checkes.

The name ``static'' analysis is justified by the fact that the anylysis is done at compile time, not at run time,

The course treats selected topics from the text book , e.g.,

  • data flow analysis and control flow analysis
  • interprocedural analysis
  • abstract interpretation
  • type- and effect systems
  • algorithmic questions

Flemming Nielson, H.R. Nielson, C. Hankin. Principles of Program Analysis. Springer-Verlag 1999.

Learning outcome

The course gives an introduction to static analysis, emphasizing some basic techniques. You will learn about the principles behind static analysis and how to apply basic analysis techniques.

 

Admission

PhD candidates from the University of Oslo should apply for classes and register for examinations through Studentweb.

If a course has limited intake capacity, priority will be given to PhD candidates who follow an individual education plan where this particular course is included. Some national researchers’ schools may have specific rules for ranking applicants for courses with limited intake capacity.

PhD candidates who have been admitted to another higher education institution must apply for a position as a visiting student within a given deadline.

Prerequisites

Recommended previous knowledge

logic, for example INF3170 - Logic.

Teaching

2 hours lecture per week.

In addition, each PhD student is expected to give an oral presentation on a topic of relevance (chosen in cooperation with the lecturer). The presentation has to be approved by the lecturer for the student to be admitted to the final exam.

Access to teaching

A student who has completed compulsory instruction and coursework and has had these approved, is not entitled to repeat that instruction and coursework. A student who has been admitted to a course, but who has not completed compulsory instruction and coursework or had these approved, is entitled to repeat that instruction and coursework, depending on available capacity.

Examination

Grading scale

Grades are awarded on a pass/fail scale. Read more about the grading system.

Explanations and appeals

Resit an examination

This course offers both postponed and resit of examination. Read more:

Special examination arrangements

Application form, deadline and requirements for special examination arrangements.

Evaluation

The course is subject to continuous evaluation. At regular intervals we also ask students to participate in a more comprehensive evaluation.

Facts about this course

Credits

10

Level

PhD

Teaching

Spring 2010

Spring 2008

Autumn 2006

Every other Spring

Examination

Spring 2008

Autumn 2006

Teaching language

English