Zohar Manna

Professor of Computer Science

Mailing Adress:
	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 is being developed to support the computer-aided formal verification of reactive, real-time and hybrid systems based on their temporal specification.

The REACT Group:

• Senior Research Associate
• Henny Sipma
• Ph.D. Students:
• Matteo Slanina
• Calegero Zarba
• César Sanchez
• Sriram Sankaranarayanan
• Ting Zhang
• Aaron Bradley

Selected Books:

• 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,1972

---

Selected publications online.

---

Ph.D. students advised

---

Recent Courses

• CS 157 (Fall 2003)  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  (Winter 2004) 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.
• CS357 (Spring 2002) . 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.