CS 711: Advanced Programming Languages
Topics in Program Analysis
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|
|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)|
|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)|
|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.
|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|
|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|
|Nov 29||Project Presentation|
|Dec 1||Project Presentation|
* will be held in Duffield 340.