| Zohar Manna
| Professor of Computer Science
| Mailing Adress:
| Gates Building, Room 481,
| Stanford University,
| CA 94305
| Phone:|| (650) 723-4364
| Fax: || (650) 725-4671
| Automated deduction: Decision Procedures, Theorem Proving.
| Semantics, specification, and verification of reactive, real-time and hybrid systems.
| Systematic development, automatic synthesis and control.
| Temporal logic and its applications. Automatic and machine-supported verification systems.
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
- Senior Research Associate
- Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems:
Progress. Unpublished, 1996. Click here to download.
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) .
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
Group home page
The Stanford home page.
The Computer Science Department home page.
The Theory Division home page.