News and Information

• Please subscribe to the cse503 mailing list.

Tentative schedule	Tuesday	Thursday
Week 1: March 27-31	Introduction and Proofs of Correctness Questionnaire Homework 1 is available. Optional Readings: Notes and more notes by David Stotts ppt slides by D. Peled	Proofs of Correctness (continued) Reading: Required: Social Processes and Proofs of Theorems and Programs, R. A. DeMillo, R. J. Lipton and A. J. Perlis, CACM 22, 5 (May 1979). Optional: Hoare's original paper, An Axiomatic Basis for Computer Programming, CACM 12, 10 (October 1969).
Week 2: April 3-7	Requirements and Specifications Homework 1 is due at the start of class (10:30 a.m.). In case you missed it, Jackson's lecture begins at roughly 1:24:30 in the video linked on this page. The slides for this week.	Requirements and Specifications (continued) Homework 2 is available. Reading: Required: The Z Notation: A Reference Manual, J.M. Spivey, Prentice Hall (2001). Chapter 1 only. Required: Statecharts: A Visual Formalism for Complex Systems, D. Harel, Science of Computer Programming 8, 3 (June 1987). Please read Sections 1-3 and skim the remainder.
Week 3: April 10-14	Statechart Specifications and Intro to Model Checking Slides for today.	Design (complexity and composition) Slides for today and next week. Send us the subject of your term paper or project by Saturday, 4/15. Reading: Required: On the Criteria To Be Used in Decomposing Systems into Modules, D.L. Parnas, CACM 15, 12 (December 1972).
Week 4: April 17-21	Design (information hiding) Homework 2 is due at the start of class (10:30 a.m.).	Design (layering and event-based systems) Reading: Optional: Designing software for ease of extension and contraction, D.L. Parnas, Proceedings of ICSE (1978).
Week 5: April 24-28	Software Architecture and Design Patterns Homework 3 is available. Reading: Required: An Introduction to Software Architecture, David Garlan and Mary Shaw, CMU-CS-94-166 (January 1994). Optional: Design Patterns: Abstraction and Reuse of Object-Oriented Design, Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides, Lecture Notes in Computer Science, 707 (1993). Optional: ArchJava: Connecting Software Architecture to Implementation, Jonathan Aldrich, Craig Chambers, and David Notkin, Proceedings of ICSE (2002).	Designing for Safety and Reliability Slides for today.
Week 6: May 1-5	Testing In case you're interested, here are the EWD Manuscripts mentioned in class.	Test Selection and Fault Isolation Slides for today. As mentioned in class, here is Andreas Zeller's Delta Debugging site (AskIgor).
Week 7: May 8-12	Analysis Slides for today. Homework 3 is due at the start of class (10:30 a.m.). Reading: Optional: Alloy FAQ Optional: Finding Bugs with a Constraint Solver, Daniel Jackson and Mandana Vaziri, Proceedings of ISSTA (2000).	Analysis References for today: Liblit et al: RAMSS 2004 PLDI 2003 PLDI 2005 Jackson: RE 2005 MSR Talk Term paper or tool evaluation due at the beginning of class. If you're doing a project, please send us a status report (1-2 paragraphs).
Week 8: May 15-19	Crosscutting Concerns (Miryung Kim) Slides for today. Class held in CSE 403 today.	Mining Software Repositories (Miryung Kim) Class held in CSE 403 today.
Week 9: May 22-26	Software Evolution Slides for this week.	Software Evolution
Week 10: May 29-June 2	Software Engineering Professionalization	Class Presentations
Final Exam Period: 10:30 a.m., June 5	Term papers, tool evaluations, and course projects due at 10:30 a.m.

Homeworks [40% of course grade]

• Homework 1, due Tuesday, April 4, at 10:30 a.m.
  Slides and more slides.
  Sample Solution
• Homework 2, due Thursday, April 13, at 10:30 a.m.
  Sample Solution
• Homework 3, due Tuesday, May 9, at 10:30 a.m.
  Sample Solution

Course project

1. A 10-15 page term paper on a one of the subjects found below (or by negotiation with the instructor and TA) [30%]
   • The objective of this paper is to take the topic, do some added reading and research into it, and provide a scholarly assessment of the state-of-the-art in the area, including open issues.
   • The paper must be written with other members of the class as the intended audience.
   • This must be done alone.  (It's fine to talk to others about the ideas and issues, but the work must be your own.)
   • Possible topics include
     • What is the state of model checking as applied to models extracted automatically from source code?
     • What are the key tradeoffs in the different underlying computational models (e.g., model checking, SAT solvers) for finding counterexamples in Nitpick and the Alcoa systems?
     • What is state-of-the-art in automated theorem provers and/or in proof assistants?
     • What is the state-of-the-art for proofs of program correctness for programs that include [side effects, exceptions, etc. --- pick one or two such language features]?
     • What is the state-of-the-art for proving correctness of object-oriented programs (not "just" abstract data type programs)?
   • Other students are looking at various issues in design patterns, extreme programming, automatic inference of invariants, etc.
   • Here are some model term papers from the first assignment:
     • Dan B. Goldman. Refactoring Tools for Extreme Programming: an Overview
     • Andrew M. Schwerin. Principles and Patterns for Security
     • Wilmot Li. Applications of Predicate Abstraction to Software Analysis
2. A tool evaluation [30%]
   • Choose a tool from our list (or propose another to David):
     • Strathcona provides users of a repository with code examples that are related to the code they are interested in.
     • Prospector is a program understanding tool that provides code examples in response to programmer queries.
     • Mylar is a user interface for Eclipse that tries to provide only the most relevant information about the current task to the programmer.
     • ShriMP is a visualization tool designed to help programmers explore large programs.
     • Daikon is a tool for dynamically detecting likely invariants in Java and C/C++ programs.
     • ESC/Java2 is a tool for finding errors in Java programs. It uses static analysis to find errors such as null dereference errors, array bounds errors, type cast errors, and race conditions at compile time. It supports pre- and post-condition style reasoning.
     • Bandera is a tool for verifying properties of Java programs using model-checking.
     • ZING is a model checker for concurrent software.
     • Purify is a tool for detecting memory errors in C/C++ programs at runtime, or debugging garbage-collection related problems in Java. A free trial version of this commercial product is available.
     • Lackwit is a tool that helps programmers with reverse engineering or restructuring tasks. The tool can detect abstraction violations, identify unused variables, functions, and fields of data structures, and detect simple errors of operations on abstract datatypes (such as failure to close after open).
     • Hyper/J is a tool that supports better separation of concerns that cross-cut standard class and method boundaries.
     • FindBugs is a bug detection tool for Java.
     • Splint (formerly LCLint) is a tool for statically checking C programs for security vulnerabilities and coding mistakes.
     • ArchJava is a small extension to Java (developed here at UW!) that lets programmers express the software architecture of a Java program within the source code. The compiler verifies that the code conforms to that architecture.
     • Alloy refers to a language and language analyzer used to verify software models, check for conformance to a specification, and generate test automatically (in progress).
     • Remember, you may request that we allow you to use an alternative tool. Many Eclipse plug-ins would be great tools to evaluate for this project.
   • Apply the tool to one or more realistic programs with the intent of developing a qualitative assessment of the strengths and weaknesses of the tool.
   • The assessment must be written with other members of the class as the intended audience; it may be written as a document or a web page.
   • This may be done in groups of up to three students.
   • Here are some model tool evaluation papers from the first assignment:
     • Amol Prakash and Mausam. Tool Evaluation : DAIKON
     • Miryung Kim and Andrew Petersen. An Evaluation of Daikon: A Dynamic Invariant Detector
     • Gang Zhao and Xin Dong. Tool Evaluation of Rational Purify
     • Bart Niswonger. Tool Evaluation: ESC/Java
3. An extensive project with a significant implementation component [60%]
   • This option requires my permission and explicit agreement on a topic.
   • Only recommended for those with a strong background both in software engineering and in system implementation.
   • This must be done alone.  (It's fine to talk to others about the ideas and issues, but the work must be your own.)

• If you do the project (C), it is due at the final exam time.
• If you do the term paper and tool evaluation (A and B), you may do them in either order with one of them due May 11 and the other due at the final exam period.