INF5906 – Selected topics in static analysis

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 include:ref: Reference resolver with name '' not found, e.g.,

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

include:ref: Reference resolver with name '' not found 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

Students who are admitted to study programmes at UiO must each semester register which courses and exams they wish to sign up for in Studentweb.

If you are not already enrolled as a student at UiO, please see our information about admission requirements and procedures.

Prerequisites

Recommended previous knowledge

logic, for example INF3170 – Logic (continued).

Teaching

2 hours lecture per week.

Examination

Oral or written exam.

Grading scale

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

Explanations and appeals

Resit an examination

Students who can document a valid reason for absence from the regular examination are offered a postponed examination at the beginning of the next semester.

Re-scheduled examinations are not offered to students who withdraw during, or did not pass the original examination.

Withdrawal from an examination

It is possible to take the exam up to 3 times. If you withdraw from the exam after the deadline or during the exam, this will be counted as an examination attempt.

Other

It is strongly recommended to attend the first lecture since it will be given important information.

Facts about this course

Credits
10
Level
Master
Teaching
Autumn 2017
Spring 2016
Spring 2014
Spring 2010
Spring 2008
Autumn 2006

Every other Spring.

INF5906 will be continued as IN5440 from Autumn 2018.

Examination

The same semester as teaching.

Exam last Autumn 2018 and Autumn 2019 for those with approved mandatory assignments.

Teaching language
English