CSE647 (Fall 2000)
Testing and Verification of Software
Scott Stoller

Table of Contents

Meeting Time and Location
Course Description
Homework Guidelines
Grading
Grading Statistics
Announcements

Meeting Time and Location

Time: 11:20am-12:40am on Tuesday and Thursday.

Location: Computer Science, Room 2212.

Office Hours: Tue and Thu, 2pm-3pm. Computer Science, Room 1429.


Course Description

This course focuses on systematic testing and automated verification of concurrent and distributed software, with an emphasis on techniques that apply to software written in standard programming languages (e.g., Java or C).

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:


Homework Guidelines

By default, assignments in this course are due by the end (midnight) of the specified day. To submit a problem set, email it to
stoller AT cs DOT sunysb DOT edu or put hardcopy under the door of Room 1429.


Grading

Here is a tentative list of weights. It is subject to minor adjustments, based on the number of homeworks and the starting date of projects.
Project50%
Exam15%
Homeworks35%

Statistics

The following statistics and histograms may be slightly inaccurate, due to late submissions, score adjustments, etc.

Item Mean Std.Dev. Histogram
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


Students with Disabilities

The Provost has required that all faculty include the following statement in their syllabus handouts:
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.


Announcements

5 Dec

Reading: The last papers we'll discuss are
Checking Temporal Properties of Software with Boolean Programs and Bebop: A Symbolic Model Checker for Boolean Program.

30 Nov

Reading: The next paper we'll discuss is A Language Framework For Expressing Checkable Properties of Dynamic Software.

22 Nov

Exam: Grading info has been added above.

21 Nov

Exam: Exam Solution is now available.

14 Nov

Project: I added an entry to the Project Errata.

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.

9 Nov

Project: Here is an Example of using RMI.

8 Nov

JavaClass: I went to the JavaClass home page and found that JavaClass has a new name. It is now called the Byte Code Engineering Library (BCEL). BCEL is installed in /home/facfs1/stoller/public/BCEL ; to use BCEL, you should include that directory in your CLASSPATH. The html documentation can be accessed here. You should also read the JavaClass paper. You will probably also benefit from the examples included in the BCEL distribution. As another example, you can also see the code for JavaChecker.

5 Nov

Project: There is now a list of Project Errata.

Project: Here is information about the Project.

3 Nov

Reading: To prepare for the project, please read about Java RMI.

2 Nov

Reading: Before Java Model Checking, we'll discuss Experience with Predicate Abstraction.

1 Nov

Reading: The next paper we'll discuss is Java Model Checking. Please start reading it.

31 Oct

Homework: Homework6-solution is now available. It references a section of Design of Java Checker.

26 Oct

Reading: Today we will also briefly discuss State-Space Caching Revisited.

19 Oct

Reading: The next paper we'll discuss is Model Checking Programs. Please start reading it.

Homework: Homework5-solution is now available.

18 Oct

Homework: Homework6 is now available.

Homework: Homework4-solution is now available.

10 Oct

Utilities: To pretty print a class file, I recommend using listclass, which comes with the JavaClass package. To use it, put /home/facfs1/stoller/public/JavaClass in your CLASSPATH, e.g., and then use (e.g.) to view the class file ./foo.class. An unrecommended alternative is /usr/bin/javap foo; javap comes with Sun JDK.

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 .

6 Oct

Homework: Homework5 is now available.

3 Oct

Reference: The definitions of dependency relations for objects and transitions that I showed on the projector today are taken from: Patrice Godefroid, Partial-order methods for the verification of concurrent systems : an approach to the state-explosion problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, 1996.

2 Oct

Homework: Homework3-solution is now available.

Homework: Homework4 is now available.

26 Sep

Reading: The next paper we'll discuss is Model-Checking Multi-Threaded Distributed Java Programs. Please start reading it. If you have difficulty printing it, let me know.

20 Sep

Reading: The next paper we'll discuss is Model Checking for Programming Languages using VeriSoft. Please start reading it.

Homework: Homework3 is now available.

19 Sep

Homework: Everyone did well on hw1, so I didn't make a solution.

15 Sep

Homework: Homework2 is now available.

11 Sep

Reading: The first paper we'll discuss is Eraser.

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.

7 Sep

Example: Queue.java is provided as an example of synchronization in Java. For now, don't worry about the try/catch statement.

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: