INF9906 - Selected topics in static analysis
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.
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.
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.
Recommended previous knowledge
logic, for example INF3170 - Logic.
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.
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.
The course is subject to continuous evaluation. At regular intervals we also ask students to participate in a more comprehensive evaluation.