Location: Computer Science, Room 2212.
Office Hours: Tue and Thu, 2pm-3pm. Computer Science, Room 1429.
For some small software systems, automated verification is possible: a tool can determine automatically whether the software satisfies given requirements. For larger systems, verification is infeasible, so we also consider techniques for systematic testing, which provide limited but well-defined correctness guarantees, for example, that a sequential program satisfies its requirements for all inputs of a certain size, or that a multi-threaded server in a distributed system satisfies its requirements whenever the clients send it at most a certain number of requests. Systematic testing techniques can also be very effective at finding bugs that would be difficult to find with conventional testing techniques.
The course will involve homeworks and a project. One or more suggestions for the project will be made; students are encouraged to suggest their own projects as well. Projects may be theoretical or implementation-oriented (ideally both!). A typical implementation project would involve enhancing a testing tool or applying a testing tool to a non-trivial software system. A typical theoretical project would involve developing a technique that makes testing more efficient.
Some experience with concurrent programming (e.g., from an operating systems course) is desirable. Prior knowledge of testing and verification techniques is not required.
Most readings will be conference or journal articles. The following paragraphs describe some research projects on software testing and verification, which are representative of what we will cover.
Static program analysis can help find limited but important classes of errors; for example, null-pointer dereferences in sequential programs, and race conditions (inappropriate locking) and deadlocks in concurrent programs. Some examples of this approach are:
Run-time monitoring tools monitor system executions, looking for common classes of errors. Typically, these techniques are passive: they neither determine which behaviors (i.e., possible executions) are of interest nor attempt to control which behaviors are explored. A good example is:
Systematic testing tools explore all possible behaviors of a system, perhaps with some limits imposed on input size, etc. Thus, they involve determining which behaviors should be explored and (if necessary) modifying the system so that the testing tool can control which behaviors are explored. Two approaches are:
bool) and model-checks boolean programs using a variant of a data-flow analysis algorithm. Boolean programs do not have dynamic heap allocation, but they have a call stack.
|hw1 (out of 20)||19.25||0.8|
|hw2 (out of 20)||16.75||0.4|
|hw3 (out of 20)||16.75||0.8|
|hw4 (out of 20)||18.5||1.5|
|hw5 (out of 30)||22.2||2.5|
|hw6 (out of 20)||14.7||2.6|
|exam (out of 50)||36.2||5.6|
If you have a physical, psychological, medical or learning disability that may impact on your ability to carry out assigned course work, I would urge that you contact the staff in the Disabled Student Services office (DSS), Room 133 Humanities, 632-6748/TDD. DSS will review your concerns and determine, with you, what accommodations are necessary and appropriate. All information and documentation of disability is confidential.
Exam: The exam on November 21 will cover material up to and including today's lecture. In other words, it covers material up to and including our discussion of the paper Java Model Checking, by Park, Stern, Skakkebaek, and Dill.
Reading: The next paper we'll discuss is Tool-supported Program Abstraction for Finite-state Verification. Please start reading it.
Project: Here is an example of How to Modify API Classes.
Project: Here is information about the Project.
Homework: Homework5-solution is now available.
Homework: Homework4-solution is now available.
Reading: In case you are interested, an extended version of my SPIN2000 paper is available as a technical report.
Reading: The JVM Specification (2nd edition) is a good reference. For a tutorial introduction to the JVM, you might want to read Under the Hood: Articles about the inner workings of Java technology .
Homework: Homework4 is now available.
Homework: Homework3 is now available.
Java: If you are unfamiliar with Java and would like to read part of a Java textbook, I have a textbook that you are welcome to borrow. Reading The Java Language Specification is fine but harder than necessary.
Homework: Homework1 due date is postponed to Mon, 18 Sep.
Course Info: Various course info has been added above. Please take a look.
Homework: Homework1 is now available. It is accompanied by hw1.java and hw1-run.
On-line Java 2 Documentation is available. The most useful links from that page are: