Department of Computer Science
CPSC 513: Integrated System Design

Meets: MW 15:30-17:00, CICSR 304.

First meeting is Monday, January 10!

Instructor: Alan Hu, CICSR 325, A J H at C S dot U B C dot C A

Links to Calendar, Readings, Assignments:

Class Calendar

Reading List

Assignments

Overview:

Course Objectives: Students completing the course will gain a solid foundation in current, practical formal verification techniques, as well as significant experience applying these techniques to a real problem of the student's choosing. The course provides necessary background for advanced research in the field, as well as general exposure to this area for students pursuing research in other areas.

Warning: The course name "Integrated System Design" is a misnomer. The course will actually be about automatic formal verification of computer systems, be they hardware, software, or some combination. I used to feel a little guilty about shifting the course towards my research area (hence this warning), but as I travel, everyone (including people from cool places like IBM, Intel, Motorola, and several start-ups) is begging me for more verification students, and my first grad students landed great jobs. So, I don't feel guilty anymore. :-) Students interested in hardware and embedded system design, rather than verification, can choose a design-oriented course project.

The first half of the course will be a crash course in automatic formal verification techniques. Topics covered will include BDDs (binary decision diagrams), equivalence of combinational circuits, reachability computation in sequential circuits, CTL model checking, and Floyd-Hoare-style software verification.

For the second half of the course, we will spend one day each week discussing advanced material (e.g., verifying pipelined microprocessors, using verification to generate tests, etc.) and current topics (e.g., Java bytecode verification, proof-carrying-code for running untrusted programs, anything else that comes up). Instead of a second lecture per week, we will meet in small groups to discuss individual projects.

Evaluation:

The course grade will be based on weekly programming assignments during the first half of the course, and on the course project. There will be no final exam. The project will be very flexible. For example, students with more theoretical leanings can tackle algorithmic or logical problems; students with more applied leanings can verify a real protocol or system (possibly from another class); and so forth. You will be encouraged to work in small groups.

Textbook:

There is no textbook for the course. Readings will come from the original research papers.

Prerequisites:

Graduate standing or consent of instructor. This area is a wonderful blend of theory, hardware, and software, but as a result, people's backgrounds will vary. I intend to make the course fairly self-contained, but familiarity with automata theory, basic digital logic, and some computer architecture will be helpful.