|Time:||Tuesdays and Thursdays, 4:35-5:55|
|Location:||Instructional Center (IC), Room 219|
Office: KACB 2320
Office hours: Tue and Thu, 3:30-4:30
|Teaching Assistant:||Ravi Mangal |
Office: Lounge area adjoining KACB 2324
Office hours: Mon 4-5, Fri 11:30-12:30
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 two components: 4 assignments (60%) and an in-class final exam (40%). 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 23||1||[PPTX] [PDF]||Introduction to Program Analysis||--||--|
|Aug 25||2||[PPTX] [PDF]||Delta Debugging||[TSE 2002]||Delta Debugging website|
|Aug 30||3||[PPTX] [PDF]||Statistical Debugging 1: Cooperative Bug Isolation||[PLDI 2003] [PLDI 2005]||CBI website|
|Sep 01||4||[PPT] [PDF]||Statistical Debugging 2: Tarantula||[ICSE 2002][ASE 2005]||Tarantula website|
|Sep 06||5||[PPTX] [PDF]||Automatic Test Generation||[ISSTA 2002]||Korat website|
|Sep 13||6||[PDF]||Intra-Procedural Dataflow Analysis: Part 1||--||--|
|Sep 15||7||[PDF]||Intra-Procedural Dataflow Analysis: Part 2||--||--|
|Sep 20||8||[PPTX] [PDF]||Context-Insensitive Pointer Analysis||[Optional: Lhotak's M.Sc. thesis]||--|
|Sep 22||9||[PPTX] [PDF]||Context-Sensitive Pointer Analysis||[PLDI 2004] [Optional: Whaley's Ph.D. thesis]||bddbddb website|
|Sep 27||10||[PPTX] [PDF]||Chord: A Program Analysis Platform for Java (Part 1)||--||Chord website|
|Oct 04||11||Same as above||Chord: A Program Analysis Platform for Java (Part 2)||--||--|
|Oct 06||12||[PDF]||Inter-Procedural Dataflow Analysis||[POPL 1995]||--|
|Oct 13||13||[PPTX] [PDF]||Type-State Checking Using Dataflow Analysis||[TOSEM 2008]||SAFE website, SAFE overview|
|Oct 20||14||[PPTX] [PDF]||Type-State Checking Using Type Qualifiers||[TOPLAS 2006]||CQual and JQual|
|Oct 25||15||[PPTX] [PDF]||Type Systems||[CRC Handbook Chapter]||--|
|Nov 01||16||[PPTX] [PDF]||Constraint-based Analysis||[TOPLAS 2007]||Saturn website|
|Nov 10||17||[PPTX] [PDF]||Software Model Checking||--||--|
|Nov 15||18||[PPTX] [PDF]||Dynamic Symbolic Execution (Concolic Testing)||[PLDI 2005]||--|
|Nov 17||19||[PDF]||Dynamic Race Detection||[SOSP 1997]||--|
|Nov 22||20||[PPTX] [PDF]||Static Race Detection||[PLDI 2006]||--|
|Nov 29||21||[PPTX] [PDF]||Systematic Concurrency Testing||[OSDI 2008]||CHESS website, CalFuzzer website|
|Dec 01||22||[PPTX] [PDF]||Deadlock Detection||[ICSE 2009] [FSE 2010]||--|
|Dec 06||23||[PPTX] [PDF]||Static and Dynamic Program Analysis: Synergies and Applications||--||--|
|Dec 08||24||--||Exam Review and Related Research at Georgia Tech||--||--|