CMPE 278 Home Page
Fall 2004

Introduction to Discrete-Systems Theory

Instructor: Luca de Alfaro

12pm-1:45pm, Tuesdays and Thursdays
Baskin Engineering 169

Office Hours: 1-2, Mondays, E2 Room 339-A, or by appointment
Email: luca@soe.ucsc.edu

Engineers design systems: from hardware designs, to embedded systems, control systems, and software components. Before a design is implemented, it is usually necessary to analyze it, to gain confidence that it is correct, and that it performs as desired. What are the concepts and tools we can use to model a system, and to analize its behavior? What are good languages to describe systems and designs, that support both simulation, and other kinds of analysis? What are the interesting properties we should check of a system, and how can we express them precisely? How can we speed up simulation, and what are the techiniques available for design verification?

The course provides an introduction to the modeling, specification, verification and analysis of discrete-state systems. The application areas range from hardware design, to embedded systems, and to real-time systems. The course will also provide a brief overview of techniques for software verification.

Class Forum

There is a web discussion forum for this class.

Prerequisites

There is no prerequisite for this course, but some mathematical background will be assumed.

Textbook

This year, I plan to follow closely the book Computer-Aided Verification, by Rajeev Alur and Thomas A. Henzinger. The book is available from UPenn, and also below, for UCSC students only. Note: I will almost certainly use a subset of the lectures below, and I will introduce some additional material on games in verification in the later part of the class.
  1. Viewgraphs of Introductory Lecture
  2. Chapter 0: Introduction
  3. Chapter 1: Reactive Modules
  4. Viewgraphs of Lecture on Chapter 1
  5. Chapter 2: Invariant Verification
  6. Viewgraphs of Lectures on Chapter 2
  7. Chapter 3: Symbolic Graph Search
  8. Viewgraphs of Lectures on Chapter 3
  9. Chapter 4: Graph Minimization
  10. Viewgraphs of Lectures on Chapter 4
  11. Chapter 5: Safe temporal logic
  12. Viewgraphs of Lectures on Chapter 5
  13. Chapter 6: Automata-theoretic Safety Verification
  14. Viewgraphs of Lectures on Chapter 6
  15. Chapter 7: Hierarchical Verification
  16. Viewgraphs of Lectures on Chapter 7
  17. Chapter 8: Fair Modules
  18. Viewgraphs of Lectures on Chapter 8
  19. Chapter 9: Response Verification
  20. Viewgraphs of Lectures on Chapter 9
  21. Chapter 10: Temporal Liveness Requirements
  22. Viewgraphs of Lectures on Chapter 10
  23. Chapter 11: Automata-theoretic Liveness Verification
  24. Viewgraphs of Lectures on Chapter 11

Viewgraphs of my Lectures

  1. Enumerative Verification, October 5.
  2. Symbolic Verification, October 8.
  3. BDDs, October 12.
  4. BDD operations, October 14.
  5. Code for forward reachability, October 14.
  6. Simulation, October 19.
  7. Abstraction, October 28.
  8. Mu-calculus, October 28.
  9. Bisimulation and CTL, November 16.
  10. Linear-time Temporal Logic, November 16.

Other Readings

  1. Computing Simulations on Finite and Infinite Graphs (Henzinger, Henzinger, Kopke).
  2. Counterexample-guided Abstraction Refinement (Clarke, Grumberg, Jha, Lu, Veith, CAV 2000).
  3. Lazy Abstraction (Henzinger, Jhala, Majumdar, POPL 2002). New!

Homework

The course will have weekly homeworks; there will be both paper-and-pencil homeworks, homeworks where you have to use tools to model and analyze small example systems, and programming assignments that will consist in the implementation of verification or analysis algorithms in various tools that are available to us.

Assigned Homeworks

Final

The course will have a final exam. There will be a review session for the final on Monday, December 6, from 2 to 4pm, in room 280 of Engineering 2.

This is the list of topics that will be covered by the final exam.

Tools

The course will be based on the tool Mocha/Chai. Mocha is a verification tool similar in the basic ideas to the commercial tools of Synopsis, Intel, Cadence, and other companies, but open source, and thus open to experimentation. We have available Chai, an advanced version of Mocha, that enables the analysis of both transition systems and games.