| Kursusnavn (dansk): | Automated Software Analysis |
| Kursusnavn (engelsk): | Automated Software Analysis |
| Semester: | Efterår 2017 |
| Udbydes under: | cand.it., softwareudvikling og -teknologi (sdt) |
| Omfang i ECTS: | 7,50 |
| Kursussprog: | Engelsk |
| Kursushjemmeside: | https://learnit.itu.dk |
| Min. antal deltagere: | 1 |
| Forventet antal deltagere: | 0 |
| Maks. antal deltagere: | 30 |
| Formelle forudsætninger: | 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: | 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: | The course starts with lectures and exercises and finishes with a project. At that point there are no more (or at least very few) lectures |
| Obligatoriske aktivititer: | Ten individual weekly assignments. A student must pass eight of them. Submission time Mondays 08:00.
— If a student fails an assignment he/she will have one chance to submit 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 submit in that particular assignment.
—In order to be eligible for a second attempt the student must have made a serious attempt to submit the original assignment. Missing or incomplete assignments are not considered serious attempts. Later submissions 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.
Be aware: The student will receive the grade NA (not approved) at the ordinary exam, if the mandatory activities are not approved and the student will use an exam attempt |
| Eksamensform og -beskrivelse: | D2G Aflevering med mundtlig eksamen der supplerer projekt. Delt ansvar for projekt., (7-scale, external exam) Submission:
- 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 submissions (see TimeEdit) and presentation: TBA, but towards the end of the course.
- 30 minutes individual oral exam.
|
| 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] |
| | |
Kursusoversigt