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. This course is motivated by the observation that there is often little interaction between research communities working on different aspects of reliability even though it seems that some of these techniques have complementary strengths and weaknesses.

In this course, we will examine three formal approaches to computer system analysis: program analysis, theorem proving and 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.

The course will be roughly structured in three parts: program analysis (taught primarily by Alex Aiken), model checking (taught primarily by Tom Henzinger) and theorem proving (taught primarily by George Necula). Some attention will be given to the aspects in which these techniques relate and complement each other.

The course can be taken for either 1 or 3 units. Students taking the 3 unit version are expected to complete a semester research project on a topic relevant to the course. 

There will be a small number of homework assignments.

The class home page for this semester is http://www.cs.berkeley.edu/~necula/294softqual. All course handouts, answers to frequently asked questions, lecture notes, and updates on assignments will be posted. Please check the home page for important course information.

Last modified: Tuesday, January 16, 2001 03:13 PM