CSCI 7135, Spring 2003
Compiler and Run-Time Analyses for Software Productivity Tools


 


Administrivia

Instructor: Amer Diwan
Office:  ECOT 743
Office hours: TuTh 2:00 - 3:30 and by appointment
Class times:  TuTh 11:00 - 12:15
Class location:  ECCR 1B06
Class web page: http://www.cs.colorado.edu/~diwan/7135-03


Goals and focus of the seminar

Tools available to programmers for coding activities---understanding, navigating through, writing, and debugging code---have improved significantly in the last decade.  For example, many of the "cool" languages today include garbage collection, which helps programmers avoid certain classes of bugs in their programs.  In this seminar we will look at recent research into a new class of software tools.  These tools range from tools for finding bugs in programs to tools for ensuring security properties in programs. 

Each class will have an assigned reading.  By 9:00 a..m. before each class, all students will submit a review for each assigned reading.  During class, the designated presenter will present the paper.  The presentation should use the same format as the review.  The presenter will need to meet with the instructor one day (or more) before the day of the presentation to discuss the presentation.  The presenter should bring a talk outline to this meeting. 

Students will also participate in a project related to the topic of the course. 

The breakdown of points for the course is as follows: Presentation and class participation (20%), Reviews (20%), Project (60%).  In order to score high in the presentation and class participation component, students should give clear and focused presentations and participate regularly in class.  In order to score high in the reviews component, students should submit reviews that clearly demonstrate that the student understands the paper well enough to evaluate it.


Schedule

This is tentative.  Please feel free to propose other papers!

Date

Papers

Software

Presenter

  Automatic verification    
1/14 Introduction and background   Amer
1/21 Parametric shape analysis via 3-valued logic (POPL 99) TVLA Amer
1/23 Putting static analysis to work for verification: A case study   Johannes
       
  Annotating programs/Extended type systems    
1/28 Extended Static Checking for Java ESC/Java Martin
1/30 A Theory of Type Qualifiers cqual Christoph
2/4 Flow-Sensitive Type Qualifiers cqual Matthias
2/6 CCured: Type-Safe Retrofitting of Legacy Code CCured Daniel
2/11 Project proposals    
2/13 CCured in the Real World (Draft: do not distribute) CCured Johannes
2/18 The Design and Implementation of a Certifying Compiler Touchstone Daniel
2/20 A Certifying Compiler for Java Touchstone Christoph
2/25 Automatically proving the correctness of compiler transformations (Draft: do not distribute)   Martin
2/27 A machine-verified code generator   Christoph
3/04 Typed assembly language   Amer
3/06 Role Analysis   Matthias
3/11 Using Data Groups to Specify and Check Side Effects   Johannes
3/13 Debugging via run-time type checking   Daniel
3/18 Project update    
4/1 Leak detection (to appear in PLDI 03) (Draft: do not distribute)   Amer
  Discovering program specifications using run-time techniques    
4/3 Discovering algebraic specifications from Java classes Ask Johannes Johannes
4/8 Quickly detecting relevant program invariants Daikon Martin
4/10 Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java Daikon
ESC/Java
Johannes
4/15 Invariant Inference for Static Checking: An Empirical Evaluation   Christoph
4/17 Tracking Down Software Bugs Using Anomaly Detection   Matthias
  Automatic Extraction of Object-Oriented Component Interfaces    
       
       
  Security    
4/22 Access Rights Analysis for Java   Daniel
     
       

Format of paper review and talk

For your talk, you should plan a 50 minute presentation, leaving the rest of the class period for discussion.  For your review, you should restrict yourself to no more than 1000 words. 

The talk and review will have the same format.  So the description below (while it refers to the talk) is equally applicable to the review.

In your talk you should assume that everyone has read the paper.  So rather than presenting the paper in detail, present only a brief summary of the paper and spend the rest of the time discussing the ideas in the paper.  Your talk should take the following format:

  1. Summary: This should summarize the key ideas in the paper and should not take up more than half the talk/review
  2. Critique
    1. Is this paper solving an important problem?
    2. Does this paper offer substantial improvement over prior work in the area?  For this you need to at least look carefully at the related works section and possibly even follow up some references.
    3. Are you convinced of the correctness of the paper? 
    4. Is the proposed tool practical for real-world situations?  If not, is it a limitation of the current implementation or of their ideas?
    5. Does the paper demonstrate that the ideas are useful? 
    6. Is the paper written well?
    7. Anything you can think of!
  3. Open problems: Are there interesting directions of future work starting from the paper?

Project details

There are two kinds of projects that we will do.  The first kind will be research and the second kind will be experience.  One of the key goals of both kinds of projects is to get you an in depth appreciation of some of the ideas brought up in this seminar.

A research project will introduce and implement some new ideas and perform experiments to understand the usefulness of the ideas.  For example, a project may extend the annotation language for one of the existing systems and evaluate whether or not it allows the system to find more bugs or report fewer false positives.  As another example, a project may implement a new system from a scratch (in one of the many infrastructures available, such as Jikes RVM, Eclipse, various bytecode-to-bytecode transformers, ...) and evaluate it.  During the first few weeks, I'll add possible ideas for research projects to this web page.  You may of course, come up with a project on your own.

An experience project will gain experience with two existing systems discussed in the seminar.  Many of the systems we will read about in class are available for download (sometimes in the source form and sometimes only in an executable form).  An example may be to take an existing significant piece of software (maybe something you have written or a standard program, example a program from the SPEC benchmark suites) and to use an existing tool (e.g., ESC) to check it.   You will need to repeat this twice (e.g., for ESC and Daikon) in order for this to count as a full project.

Each project will have three parts, proposal, stage 1, and stage 2 (see schedule for the due dates for each stage). 

For a proposal,  you will need to write a 5000 word or less document describing your project.  For a research project, your proposal should describe what research you will undertake, the motivation for the research, what infrastructure you will use, the related work in the area, and what you will deliver for stages 1 and 2.  In other words, for a research project, it is up to you to break down the project into two stages.  For a experience project, your proposal should indicate the two systems that you will use and the program(s) you will use with each system.   You will need to finish one of the systems for stage 1 and the other for stage 2.  Your proposal should be concrete and convincing;  i.e., reading it should convince me that you have a good chance of successfully doing the project.  For example, if you are planning to use certain tools/systems in your project, you should make sure you have downloaded and installed them and verified that they work as expected.

For stages 1 and 2, you need to submit a document describing in detail what you did in that stage.  Watch this space for more details on the format of your stage 1 and 2 reports.


How to submit your reviews and project documents

Everything should be submitted electronically as follows:

Some useful things to know about online submission