Topics in Software Engineering

Papers for Presentations or possible future reading

For some projects, such as Metal or Alloy, I've list several papers, but a presentation may be based on only some (perhaps one or two) of these.

Course Outline

Reliability of computer systems is an important practical issue and researchers have devised numerous techniques and tools aimed at improving the reliability of both software and hardware components.

In this course, we will examine five main approaches to computer system analysis:

• testing
• type systems
• program analysis
• theorem proving
• model checking

The presentation will be mostly in the context of improving the reliability of software and the emphasis will be in exposing the strengths and weaknesses of each technique, along with the similarities and differences between them. The ultimate goal of the course is to gain insight into what kinds of integrations of these formal techniques is possible and beneficial, as well as gaining an understanding of the current state of the art in software validation.

Some experience with concurrent programming (e.g., from an operating systems course) is desirable. Prior knowledge of testing and verification techniques is not required.

There will be five homeworks, one every two weeks. Think of these as "take home exams."  Homeworks will develop your skills in the more theoretical aspects of the course, though some programming may also be required. The homework assignments are in the schedule above. These homeworks should be handed in on paper at the start of class on the due day.

Type systems: Traditional views of types are as descriptors of data format, e.g. as integers, strings, and pointers. While types in this view have an unquestioned benefit on software dependability, types can be used to also express higher level program invariants. For example, linear type systems can ensure that a program always deallocates resources it allocates, thus preventing leaks. Types can be used to prevent race conditions and deadlock. We will examine a tools and approaches that aim to use types to improve software dependability, including CQual, race-free Java, and others.

Model Checking: Model checking was first popularized as a means to hardware verification, but recent advances have illustrated that it can be effectively applied to software. We will explore the approaches behind model checking, and experiment with freely available tools, like Bogor and JPF. We will also consider the relationship between model checking, testing, and type systems.

Testing and Dynamic analysis: A drawback of all of the static techniques above is that they must assume various levels of conservatism because they consider all possible executions of a program. By contrast, dynamic analysis examines particular runs of a program at a finer granularity. We will examine how dynamic analysis can be used to discover program properties, as in Daikon, or find common classes or errors.

Theorem Proving: A wide variety of tools use automated theorem proving to establish the truth of certain properties in programs. We will examine both the tools that employ theorem provers, like ESC/Java

Program Analysis: We will consider the cost and quality of various tranditional forms of static analysis.

Presentations

Each student will give one lecture about a particular tool or technique, starting at roughly halfway through the quarter. Presentation quality is important: read your papers early and be sure you fully understand them. I will be available for help, if you need it. Be sure that you have prepared a good presentation (consider practicing it beforehand). 

Presentations will be judged based on the following criteria:

• understanding: does the presenter understand the material?
• thoughtfulness: does the presenter have insights and opinions beyond what was in the paper?
• background/perspective: did the presenter read background papers?
• clarity: can the audience understand the presentation? is the "big picture" clear? are there useful examples?
• materials: do the slides or use of blackboard illustrate and support the talk? are there diagrams to help convey the technicalities? (when your talk gets into deep territory, a diagram is worth 10K words)
• delivery: has the the presenter practiced?
• non-regurgitation: did the presenter do something beyond simply typing sections of the paper as bullet points? did the presenter motivate the ideas in their own words or just state ideas from the paper verbatim?
• answering questions: can the presenter handle questions from the audience?

The majority of the course will consist of reading and discussing web-available technical papers on the above topics, and in using tools.  The final grade will be computed as follows:

• Class Participation. (35%) This consists of discussion in class, and discussion on the course newsgroup regarding the papers we read and the tools we use.
• Homeworks. (50%)
• Presentation. (15%)