Zohar Manna

Professor of Computer Science

Mailing Address:
	Gates Building, Room 481,
	Stanford University,
	Stanford,
	CA 94305
Email:	manna@cs.stanford.edu
Phone:	(650) 723-4364
Fax:	(650) 725-4671

Research Interests

The STeP (Stanford Temporal Prover) system supports the computer-aided formal verification of reactive, real-time and hybrid systems based on their temporal specification.

Selected Books

• Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, 2007.

• Zohar Manna. Mathematical Theory of Computation. (Reprint), Dover, 2003.

• Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Progress. Unpublished, 1996. Click here to download.

• Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.

• Zohar Manna and Richard Waldinger. The Deductive Foundations of Computer Programming. Addison-Wesley, 1993.

• Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems:Specification. Springer-Verlag, 1992.

• Zohar Manna. Mathematical theory of computation. McGraw Hill, 1974

Translations:

Czech	Italian	Japanese	Hungarian	Bulgarian	Russian

---

Selected publications online

---

Doctoral Descendants

  Verification: Theory and Practice (Dedicated to Zohar Manna on his 64th Birthday). Springer-Verlag, LNCS 2772, 2004.

---

Recent Courses

• CS156 (Fall 2008) Calculus of Computation. This course presents an introduction to software verification. It covers the foundation of reasoning about programs from first principles: specifications and program annotations are represented by first-order logic formulas; program statements are represented by first-order transformation relations. It also covers decision procedures for arithmetic over the reals, for arithmetic over the integers, for recursive data structures and arrays, and for combinations of theories.
• CS 157 Introduction to logic for computer science. An elementary exposition, from a computational point of view, of propositional logic, predicate logic, axiomatic theories, and theories with equality and induction. Basic notions: interpretations, models, validity, proof. Automated deduction: polarity, skolemization, unification, resolution, equality, strategy along with applications.
• CS 256 (Spring 2008) Formal methods for reactive and concurrent systems. This course covers specification and verification of reactive systems, that is, systems that maintain an ongoing interaction with their environment. Verification methods are presented for proving that such reactive systems meet their specifications, expressed in temporal logic. Verification methods include deductive methods based on theorem proving, as well as algorithmic methods based on model checking. The course also places emphasis on temporal logics , their expressive power and the applications of automata theory in formal methods.
• CS 357 Topics in Formal Methods. This course covers specification and verification of reactive systems, with emphasis on real-time and hybrid systems. Verification methods are discussed for proving that such reactive systems meet their specifications, with emphasis on methods that combine deductive and algorithmic techniques, tree and alternating automata and their applications to Formal Methods.

---





The STeP Group home page

The Stanford home page.

The Computer Science Department home page.

The Theory Division home page.