|Time:||Mondays and Wednesdays, 4:35-5:55 pm|
|Location:||Room 1103, UA Whitaker Biomedical Engineering Building|
Office: Room 2320, Klaus Advanced Computing Building
Office hours: 3:30-4:30 pm before class
|Teaching Assistant:||Xin Zhang |
Office: Room 2319, Klaus Advanced Computing Building
Office hours: 3:30-4:30 pm before class
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.
Intended Audience: The course is intended for students who would like to: 1) pursue research in the specializations of programming languages, compilers, and software engineering; 2) pursue research in other specializations of computer science (e.g., information security or systems) that may involve applying program analysis to problems in their domain; and 3) become more productive software engineers in industry.
Evaluation: Students will be evaluated based on three components: take-home assignments (50%), an in-class midterm exam (25%) and an in-class final exam (25%). Assignments will be of two kinds: (1) using a program analysis tool based on a technique presented in class, and reporting your findings, or (2) implementing a program analysis algorithm in Java using the Chord program analysis framework.
Pre-Requisites: There are no pre-requisites for the course but sudents will be expected to do programming in Java for some assignments. The course is open to both MS and PhD students. Undergraduate students require permission from the instructor. The course counts as an elective in the MS CS program for the specializations of "Information Security" and "Databases and Software Engineering (DB+SE)", and as a breadth component in the PhD CS program for the areas of "Programming Languages and Compilers" and "Software Methodology and Engineering".
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 assignments individually unless explicitly told otherwise. You may discuss the assignments with classmates but you may not copy any solution (or any part of a solution) from a classmate.
|Aug 18||Quiz and Solution||Course logistics and quiz||--|
|Aug 20, Aug 25||[PPTX] [PDF]||Introduction to program analysis||--|
|Aug 27, Sep 03||[Part 1] [Part 2]||Intra-procedural dataflow analysis||--|
|Sep 08, Sep 10||[PPTX] [PDF]||Pointer analysis: Part 1||[Lhotak's M.Sc. thesis]|
|Sep 15||[PPTX] [PDF]||Chord: A program analysis platform for Java||[Chord website]|
|Sep 17||[PPTX] [PDF]||Pointer analysis: Part 2||[Whaley's Ph.D. thesis]|
|Sep 22||[PDF]||Inter-procedural dataflow analysis||[POPL 1995 paper]|
|Sep 24, 29||[PPTX] [PDF]||Type-state checking using dataflow analysis||[TOSEM 2008 paper] [Experience paper]|
|Oct 01||[PPTX] [PDF]||Type-state checking using type qualifiers||[TOPLAS 2006] [CQual and JQual]|
|Oct 06||--||Midterm exam||--|
|Oct 08||--||Review of midterm solutions||--|
|Oct 13, 15||--||No class (Fall recess)||--|
|Oct 20, 22||[PPTX] [PDF]||Type systems||[CRC Handbook Chapter]|
|Oct 29||[PPTX]||Constraint-based analysis||[TOPLAS 2007], [Saturn website]|
|Nov 03, Nov 05||[PPTX] [PDF]||Dynamic symbolic execution||[PLDI 2005]|
|Nov 17, Nov 19||[PPTX] [PDF]||Software model checking||[SLAM website], [BLAST website]|
|Nov 24||[PPTX] [PDF]||Fault localization: Part 1 (Cooperative bug isolation)||[PLDI 2005]|
|Nov 26||[PPTX] [PDF]||Fault localization: Part 2 (Delta debugging)||[TSE 2002]|
|Dec 01||[PDF]||Dynamic concurrency analysis||[SOSP 1997]|
|Dec 03||--||Review of final exam material||--|
|Dec 08||--||Final exam||--|