CIS 670: Program Analysis, Fall 2007
Class: Mon Wed 1.30 -- 3, Levine 612 (note revised time and location)
First lecture: Monday, Sept 10
Office hours: Tues 2-3, Levine 609, and by appointment
Introduction
Program analysis refers to a broad collection of algorithms and tools for
statically analyzing programs to deduce information about their runtime behavior.
While program analysis techniques were originally developed for
optimizing compilers, this course will emphasize their
contemporary application in finding bugs in programs.
Based on recent advances, program analysis tools can now discover programming errors,
such as potential out-of-bounds array references,
stack overflows, and data races, in large scale code bases, and are routinely used
in software development to improve programmer productivity.
This course will span logical foundations, algorithmic techniques,
industrial-strength tools, and current research directions in program analysis.
Topics include
- Theory: Abstract interpretation, dataflow analysis, fixpoint calculi
- Algorithms: CFL reachability, flow-sensitive analysis, path sensitive analysis
- Specific analyses: Pointer analysis, shape analysis, worst-case execution time analysis
- Analysis in practice: Scalability, SAT solvers, tools in industry
- Software model checking: Predicate abstraction, counter-examples and refinement
- Hot topics: Multi-threaded programs and race detection, analyzing binaries,
analysis for security properties,
analysis for resource consumption
Prerequisites
The course requires basic knowledge of
programming languages, algorithms, data structures,
automata theory, and propositional(boolean) logic (CIS 500, 502, CIS 511, or equivalent).
If you need more information to decide, contact the instructor.
Note: The content of this course significantly differs from CIS 673 (Computer Aided
Verification) offered in Fall 2006.
Reading
The course will use a variety of sources.
A preliminary list includes:
- Principles of Program Analysis. Nielson, Nielson, and Hankin, Springer, 1999. (Chapter 2)
- Parametric shape analysis via 3-valued logic.
Sagiv, Reps, and Wilhelm, TOPLAS 2002.
pdf
- Abstract interpretation: a unified lattice model for static analyis of programs
by construction or approximation of fixpoints.
Cousot and Cousot. POPL 1977.
pdf
- Program analysis via graph reachability.
Reps, 1998.
pdf
- Saturn: A scalable framework for error detection using Boolean satisfiability.
Xie and Aiken, TOPLAS.
pdf
- The ASTREE Static Analyzer
- Determining bounds on execution times, Wilhelm
- CheckFence: Checking consistency of concurrent data types on relaxed memory models
- CUTE: A concolic unit testing engine for C; Sen, Marinov, Agha; FSE 2005 pdf
- Logics and automata for software model checking.
Alur and Chaudhuri, 2006.
pdf
Schedule
- Sept 10, 12, 17, 19: Dataflow Analysis
Sections 2.1, 2.3, 2.4 of Nielson, Nielson, Hankin
- Sept 24, 26: Program analysis via graph reachability
PLDI'00 Tutorial by Reps
- Oct 1, 3: Abstract interpretation
Guest lecturer: Sriram Sankaranarayanan (NEC Labs).
Lecture 1 and
Lecture 2
- Oct 8, 10: Shape analysis
CAV'04 Tutorial by Reps
- Oct 15: Fall break
- Oct 17, 22: Scalable program analysis using SAT solvers
Saturn overview by Aiken,
Memocode'06 talk by Aiken
- Oct 22, 24: Modern SAT solvers
Talk by Malik
- Oct 27, 29: Software model checking with SLAM
Ball and Rajamani. PLDI 2003 tutorial.
ppt
- Nov 5: Software model checking with BLAST
Henzinger, Jhala, Majumdar,
SPIN 2005 tutorial
- Nov 7: No class
- Nov 12: Worst-case execution time analysis
WCET tutorial by Wilhelm
- Nov 14: CheckFence project at Penn
- Nov 19, 21: Concurrency analysis (Guest lecturer: Vineet Kahlon)
Lecture slides
- Nov 26: Combining symbolic and random testing
Concolic testing by Sen
and DART by Godefroid
- Nov 28: Randomized abstract interpretation (Guest lecturer: Sriram Sankaranarayanan)
- Dec 3: Analysis of binaries (Guest lecturer: Gogul Balakrishnan)
slides
Project
The grade will be based on a project. The project can be done in groups
of two.
Useful links to possible tools:
Project schedule
- Oct 10: Decide on your team and tool
- Oct 31: Get familiar with the tool infrastructure and propose a project
- Dec 5: Project report due
- Dec 10, 12: Project presentations
Maintained by Rajeev Alur