| Time: | 3:05-4:25 pm, Mon and Wed |
| Location: | CoC 102 |
| Instructor: | Mayur Naik Email: naik@cc.gatech.edu Office: KACB 2320 Office hours: By appointment |
| Teaching Assistant: | Ravi Mangal Email: rmangal3@gatech.edu Office: KACB 2319 Office hours: By appointment |
Objectives: Aspects of software development besides programming, such as testing, debugging, and verification, comprise over 50% of the cost of software development. Modern technology has come a long way to aid programmers with these aspects. At the heart of this technology lies program analysis: a body of work that concerns discovering facts about a given program. Many diverse program analysis approaches exist, each with their own strengths and weaknesses. This course will cover a broad spectrum of these approaches, including type systems, dataflow analysis, model checking, theorem proving, and dynamic analysis, as well as their combinations. Both the principles underlying these approaches and hands-on experience with using and implementing tools that realize these approaches will be covered. A mix of basic and advanced topics will be covered.
Learning Outcomes: The course is intended for students who would like to:
Pre-Requisites: There are no pre-requisites for the course but students will be expected to be comfortable with a) mathematical and logical reasoning, and b) programming in a language like Java. The course is open to both MS and PhD students. Undergraduate students require permission from the instructor.
Evaluation: Students will be evaluated based on the following components:
| Component | Weight |
| In-class mid-term exam | 20% |
| In-class final exam | 30% |
| Programming assignments | 25% |
| Project and presentation in team of 2-3 | 25% |
Course Material: There is no required textbook; all relevant materials will be made available on-line.
Academic Honesty: Students are expected to abide by the Georgia Tech Honor Code. Honest and ethical behavior is expected at all times. All incidents of suspected dishonesty will be reported to and handled by the office of student affairs. You will have to do all take-home work individually unless explicitly told otherwise. You may discuss it with classmates but you may not copy any solution (or any part of a solution) from a classmate.
| Date | Handout | Topic | Reading | More Resources |
| Aug 20 | [PPTX] [PDF] | Introduction to program analysis | -- | -- |
| Aug 22 | [PDF] | Quiz | -- | -- |
| Aug 27 | [PDF] | Intra-procedural dataflow analysis: Part 1 | -- | -- |
| Aug 29 | [PDF] | Intra-procedural dataflow analysis: Part 2 | -- | -- |
| Sep 5 | [PPTX] [PDF] | Pointer analysis: Part 1 | [Lhotak's M.Sc. thesis] | -- |
| Sep 12 - 17 | [PPTX] [PDF] | Chord: A program analysis platform for Java | [Whaley's Ph.D. thesis] | Chord website, bddbddb website |
| Sep 19 | [PPTX] [PDF] | Pointer analysis: Part 2 | [PLDI 2004] | -- |
| Sep 24 | [PDF] | Context-sensitive analysis | [POPL 1995] | -- |
| Sep 26 | [PPTX] [PDF] | Type-state checking using dataflow analysis | [TOSEM 2008] | SAFE website, SAFE overview |
| Oct 1 | [PPTX] [PDF] | Type-state checking using type qualifiers | [TOPLAS 2006] | CQual and JQual |
| Oct 3 | List of projects (preferences due by Oct 10) | |||
| Oct 8 | In-class midterm | |||
| Oct 10 | Midterm solutions | |||
| Oct 22 | [PPTX] [PDF] | Type systems | [CRC Handbook Chapter] | -- |
| Oct 24 | [PPTX] [PDF] | Constraint-based analysis | [TOPLAS 2007] | Saturn website |
| Oct 29 | [PPTX] [PDF] | Software model checking | -- | SLAM website, BLAST website |
| Oct 31 | [PPTX] [PDF] | Dynamic symbolic execution | [PLDI 2005] | -- |
| Nov 14 | Dynamic symbolic execution (contd.) | |||
| Nov 19 | [PPTX] [PDF] | Static race detection | [PLDI 2006] | |
| Nov 26 | [PPTX] [PDF] | Deadlock detection | [ICSE 2009] [FSE 2010] | |
| Dec 3 | Project Presentations (Part 1) | |||
| Dec 5 | Project Presentations (Part 2) |