CS 8803: Foundations of Programming Languages

Fall 2012

[Course Information] [Course Description] [Syllabus]

Course Information

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

Course Description

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:

ComponentWeight
In-class mid-term exam20%
In-class final exam30%
Programming assignments25%
Project and presentation in team of 2-325%

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.

Syllabus

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)