17-654/17-754 Analysis of Software Artifacts

Spring 2005
Tuesdays/Thursdays 10:30-11:50am
Newell-Simon Hall 1305
12 units
Professor Jonathan Aldrich
Office hour: Wednesday 1pm in Wean Hall 8212
TA Nicholas Sherman, office hour: Tuesday 1pm in the MSE Cave
TA Dean Sutherland, office hour: Thursday 4pm in Wean Hall 8130

This course fulfills the Analysis STAR requirement for the Software Engineering Ph.D. program.

IMPORTANT NEWS: The bookstore cannot get the recommended textbook until January 31 (probably because it is being reprinted). The textbook is recommended but not absolutely required. Most of the readings from the text will be in January and so waiting until the 31st to get the book is not a good idea. Students who want a copy of the text in January should get it from an online bookseller. Amazon and Barnes&Noble are apparently out of stock, but you can try some others from Yahoo's list.

Overview

Analysis is the systematic examination of an artifact to determine its properties. This course will focus on analysis of software artifacts--primarily code, but also including analysis of designs, architectures, and test suites. We will focus on functional properties, but also cover quality attributes like performance and security. In order to illustrate core analysis concepts in some depth, the course will center on static program analysis; however, the course will also include a breadth of techniques such as testing, model checking, theorem proving, dynamic analysis, and type systems.

Concern for realistic and economical application of analysis will also be evident in a bias towards analyses that are scalable and incremental. The course emphasizes the fundamental similarities between analyses (in their mechanism and power) to teach the students the limitations and scope of the analyses, rather than the distinctions that arose historically (static vs. dynamic, code vs. spec). The course will balance theoretical discussions with lab exercises in which students will apply the ideas they are learning to real artifacts.

After completing this course, students will:

know what kinds of analyses are available and how to use them
understand their scope and power, when they can be applied and what conclusions can be drawn from their results
have a grasp of fundamental notions sufficient to evaluate new kinds of analysis when they are developed
have some experience selecting and writing analyses for a real piece of software, applying them and interpreting the results

In addition, Ph.D. students taking the 17-754 version of the course will gain a broad overview of the analysis research literature and in-depth knowledge of a particular sub-area through a course project.

A presentation describing the course is also available.

Reading

The recommended textbook for the course will be Principles of Program Analysis by Nielson, Nielson, and Hankin. The CMU bookstore will not be able to get the book until January 31, but most of the reading in the book will be done before then (the material will also be covered in class). Students who want the book before then should get it from an online retailer such as the list of textbook sellers at Yahoo. The course text will be supplemented with papers from the research literature and handouts prepared by the instructor.

Evaluation

Evaluation will be based on the following approximate percentages:

10% reading questions and participation
44% homeworks and programming
16% midterm exam
30% final project

The homeworks will include:

Questions covering the theory of various analysis technologies, as well as their benefits and limitations in concrete engineering settings (the exams will cover similar material in an evaluative setting)
Applying commercial and research analysis tools to software artifacts and reporting on the results (in writing and with an in-class presentation)
Writing simple analyses and applying them to verify engineering properties of code

Ph.D. students will undertake a more in-depth project, to be arranged with the instructor. Grading breakdowns and homework requirements for Ph.D. students may be slightly adjusted to reflect the greater emphasis on the project. The project will include at least a written report (whose length will depend on the specific project and whether it has an additional implementation component) and a presentation in class. Example projects might include:

A literature survey in a sub-area of analysis, describing what is the current state of the art and what are open research questions in the area.
A comparative evaluation of multiple analysis techniques or tools, based on experience applying the tools to software artifacts.
The development of an interesting new analysis technique, or application of an existing technique to a new problem domain.

Tentative Schedule

Handouts are the same as slides, but are printed 6 to a sheet to save paper.

Date	Topic	Readings	Slides	Assignment Due
Dataflow Analysis
Jan 11	Motivating Example: Fluid		slides, handout
Jan 13	Course Introduction; Program Analysis	NNH 1.1-1.3, 1.7-1.8	course intro slides, handout program analysis slides, handout
Jan 18	Data Flow Analysis	NNH 1.1-1.3, 1.7-1.8	slides, handouts
Jan 20	More Data Flow Analyses	NNH 2.1, 2.3, Appendix A.1	slides, handouts
Jan 25	More Data Flow Analyses	NNH 2.1	slides, handouts
Jan 27	Data Flow Lattices	NNH 2.3	slides, handouts	Homework 1, Homework 1 Addendum
Feb 1	Soundness	NNH 2.2 (optional)	slides, handouts
Feb 3	More Lattices and Soundness	NNH 2.2 (optional)	slides, handouts	Homework 2, latex sources
Feb 8	Soundness and Workflow Algorithms	NNH 2.4	slides, handouts
Feb 10	Bug-finding Dataflow Analysis	A Static Analyzer for Finding Dynamic Programming Errors	slides, handouts	Programming 0
Feb 15	Incremental Concurrency Analysis in Fluid	Assuring and Evolving Concurrent Programs: Annotations and Policy	slides, handouts
Feb 17	User-defined property checking	Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions	slides, handouts
Feb 22	Typestate Checking	The Fugue Protocol Checker: Is Your Software Baroque?	slides, handouts	Reading Questions
Feb 24	Daikon: Dynamic Analysis	Dynamically Discovering Likely Program Invariants to Support Program Evolution	slides, handouts	Programming 1
Model Checking
Mar 1	Introduction to model checking		handouts
Mar 3	Complexity Reduction Techniques	Clarke et al., Model Checking, ch. 1-4	handouts
Mar 7-11	No Class - Spring Break

Mar 15	Software Verification	Clarke et al., Model Checking, ch. 6-7	handouts
Mar 17	State/Event-based model checking	State/Event-based Model Checking, additional optional reading	handouts
Mar 22	Component Substitutability analysis	Papers on Automated Deadlock Detection, Component Substitutability Analysis for single and multiple upgrades	slides, handouts
Analysis Through the Software Lifecycle
Mar 24	Testing		slides, handouts
Mar 29	Regression Test Prioritization	Effectively Prioritizing Tests in Development Environment	slides, handouts	Reading Questions
Mar 31	Model Checking discussion session and presentations			Model Checking Lab due in class (available on Blackboard)
Apr 5	Model-Based Test Coverage	A Theory of Predicate-Complete Test Coverage and Generation	slides, handouts	Reading Questions 1-page project proposal due Suggested tool list for project
Apr 6	Midterm Review		slides, handouts
Apr 7	Defect Prediction	Predicting Field Problems Using Metrics Based Models. Sections 1-4. short (required) version, full version	slides, handouts	Programming 2 and the CSGuestbook.zip application Framework code available on Blackboard Take Home Midterm out NOW on Blackboard
Apr 12	Reverse engineering	Reverse Engineering and Design Recovery - A Taxonomy	handouts	Reading Questions (PDF and LaTeX) Take home midterm due (see Assignments section of Blackboard)
Apr 14	No Class - Spring Carnival
Analysis for Quality Attributes
Apr 19	Security: Attack Graphs	Tools for Generating and Analyzing Attack Graphs	slides, handouts	optional Reading Questions (LaTeX source)
Apr 21	Security: Privilege Separation and Timing Attacks	optional: Privtrans: Automatically Partitioning Programs for Privilege Separation and Remote Timing Attacks are Practical	slides, handouts	mid-project progress reports due
Apr 26	Re-Engineering	optional: Why Reengineering Projects Fail	handouts	optional Reading Questions (LaTeX source)
Apr 28	Reflexion Models	optional: Reengineering with Reflexion Models: A Case Study	slides, handouts
May 3 Wean 5409 10:30-1:30	Final Project Presentations
May 5				Final Project reports due Example reports: 1 and 2