CS 711: Advanced Programming Languages

Topics in Program Analysis

Instructor:  Radu Rugina
Time:  Tuesday, Thursday 2:30 - 3:30 pm
Place:  Upson 5130
Prerequisites:  CS412 and CS411/CS611, or permission of the instructor.

This seminar covers advanced topics in program analysis. We will look at analysis techniques that target various programming constructs, including procedures, virtual calls, objects, pointers, recursive structures, threads, and executable code. We will discuss the use of types, program annotations, and specifications in combination with static analysis; and the applications of static analysis to program optimization, verification, and error detection. Finally, we will look at approaches for the automatic generation of static analyzers.

The reading list includes relatively recent papers in each area, as shown in the tentative schedule below. The format of each lecture consists of a 35 min. presentation, and a discussion of the subject for the remaining 25 min. Students who enroll in this class are expected to read each of the papers and express opinions during the discussions; present 1-2 papers; and complete a small course project.

A relevant book that covers several of the topics below is "Principles of Program Analysis", by Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Springer 1999, ISBN 3-540-65410-0.

Date Topics / Papers Presenter
Aug 30  Course Overview (slides) Radu Rugina
   Inter-Procedural Analysis  
Sep 1   Precise interprocedural dataflow analysis via graph reachability (POPL'95) (slides) Radu Rugina
Sep 6   Fast static analysis of C++ virtual function calls (OOPSLA'96) (slides) Nate Nystrom
    Fast interprocedural class analysis (POPL'98)  
    Points-to Analysis  
Sep 8   Pointer analysis: haven't we solved this problem yet? (PASTE'01) (slides) Radu Rugina
    Context-sensitive inter-procedural points-to analysis in the presence of function pointers (PLDI'94)  
Sep 13 *   Points-to analysis in almost linear time (POPL'96)  (slides) Maks Orlovich
    Program analysis and specialization for the C programming language (DIKU'94)  
    Shape Analysis  
Sep 15   Solving shape-analysis problems in languages with destructive updating (POPL'96) (slides) Radu Rugina
Sep 20   Shape analysis via 3-valued logic (POPL'99) (slides) Ruijie Wang
Sep 22   Region-based shape analysis with tracked locations (POPL'05) (slides) Radu Rugina
    Static Error Detection  
Sep 27  ESP: path-sensitive program verification in polynomial time (PLDI'02) (slides) Lucja Kot
Sep 29  A first step towards automated detection of buffer overrun vulnerabilities (NDSS'00) (slides) Steve Chong
Oct 4  Code Sonar - an automated bug-finding tool for C/C++
 Invited speaker: David Vitek, GrammaTech, Inc.		 David Vitek
    Analysis of Executable Code  
Oct 6   Alias analysis of executable code (POPL'98) (slides) Xin Qi
Oct 13   Static Analysis of Executables to Detect Malicious Patterns (USENIX'03) (slides) K. Vikram
Oct 18   Analyzing Memory Accesses in x86 Executables (CC'04) Siggi Cherem
    Analysis of Multithreaded Programs  
Oct 20  Parallelism for free: efficient and optimal bitvector analyses for parallel programs  (TOPLAS'96) (slides) Aaron Kimball
Oct 25  Verifying safety properties of concurrent Java programs using 3-valued logic (POPL'01) Radu Popovici
    Type-Based Analysis  
Oct 27  Type-Based Race Detection in Java (PLDI'00) Rohit Fernandes
Nov 1  Ownership types for flexible alias protection (OOPSLA'98) Radu Popovici
   User annotations and specifications  
Nov 3  Modular Checking for Buffer Overflows in the Large (MSR) Aaron Kimball
Nov 8  The Pointer Assertion Logic Engine (PLDI'01) (slides) K. Vikram
Nov 15  ESC Java (PLDI'02) / Spec# (CASSIS'04) (slides) Michael Clarkson
    Automatic Generation of Static Analyses  
Nov 17  HOIST: a system for automatically deriving static analyzers for embedded systems (ASPLOS'04)   Siggi Cherem
Nov 22  Symbolic implementation of the best transformer (VMCAI'04) Xin Qi
   Project Presentations  
Nov 29  Project Presentation  
Dec 1  Project Presentation  

 * will be held in Duffield 340.