IT-Universitetet i København
 
  Tilbage Kursusoversigt
Kursusbeskrivelse
Kursusnavn (dansk):Tools and Methods for Automatic Detection of Errors in Programs 
Kursusnavn (engelsk):Tools and Methods for Automatic Detection of Errors in Programs 
Semester:Efterår 2015 
Udbydes under:cand.it., softwareudvikling og -teknologi (sdt) 
Omfang i ECTS:7,50 
Kursussprog:Engelsk 
Kursushjemmeside:https://learnit.itu.dk 
Min. antal deltagere:
Forventet antal deltagere:
Maks. antal deltagere:30 
Formelle forudsætninger:Formal prerequisites:
Discrete mathematics
Introductory programming 
Læringsmål:Describe formally the meaning of a wide range of programming constructs
Explain fundamental concepts/techniques/results regarding semantics of programming languages
Reason About semantic descriptions of programming languages
Prove simple properties (structural induction)
Analyze programs (program analysis)
Discuss possibilities and limitations of automated static analysis 
Fagligt indhold:Please note, that due to technical challenges, changes may occur before the start of the semester (week 35) – this applies to all sections of the course description.

This course is about "Automated Software Analysis". You will learn
how to automatically analyze software and how code analyzers work
(such as "Coverity" and Facebook's "Infer" code analysis tool).

The course is devided into four parts:

First, we will study "operational semantics", which we will need as a
foundation to understand and reason about what a program does. (Also,
we will use this to establish properties of the programming languages
themselves.)

Second, we will look at how to automatically detect errors in
programs. Specifically, we will study "dataflow analysis" which is
based on operational semantics and capable of automatically tracking
how data flows through a program.

Third, we cover program analysis "tools" designed for automatically
finding errors in programs. We will use these tools on non-trivial
programs to help ensure their correctness and go into depth on exactly
how these tools obtain their results.

Finally, the students will do a project in small groups in either of
the three parts above (your choice). The project can be either
theoretically or practically oriented (or a combination of both). 
Læringsaktiviteter:

Obligatoriske aktivititer:- Ten individual weekly assignments. A student must pass eight of them. Handin time Mondays 08:00.

— If a student fails an assignment he will have one chance to hand it in again the following week with the same deadline as the next assignment. If a student fails that assignment as well there will be no more opportunities to hand in that particular assignment.

—In order to be eligible for a second attempt the student must have made a serious attempt to hand in the original assignment. Missing or incomplete hand ins are not considered serious attempts. Later hand ins are allowed only under very special circumstances.

— There will be a mandatory lecture where the projects are presented in front of the class. Exemptions can be given in very special circumstances, but otherwise attendance and participation is mandatory. 
Eksamensform og -beskrivelse:X. experimental examination form (7-scale; external exam)

Hand-in
- One four-week project in groups of two (minimum) or three (maximum) with shared responsibility.

— The project can focus on the theoretical aspects of the course, the practical aspects, or a combination of both.

— A report of 15 pages must be submitted.

— Deadline for project hand-in (see TimeEdit) and presentation: TBA, but towards the end of the course.

- 30 minutes individual oral exam.

Duration of oral exam: 30 minutes  

Litteratur udover forskningsartikler:Relevant excerpts will be provided

- "Principles of Program Analysis" (p. 1-29)
[F.Nielson && H.R.Nielson && C.Hankin, 1999]

- "Semantics with Applications" (p. 19-50)
[H.R.Nielson && F.Nielson, 1992]

- "Lecture Notes on Static Analysis"
[M.Schwartzbach, 2000'ish]

- “How to Solve Recursive Equations"
[C.Brabrand, 2008]

- "Relations as Least-Fixed Points of Inference Systems"
[C.Brabrand, 2008] 
 
Undervisere
Følgende personer underviser på kurset:
NavnStillingUndervisertypeIndsats (%)
Claus Brabrand Lektor(ITU) Underviser 55
Jesper Bengtson Lektor(ITU) Kursusansvarlig 45