Zohan Manna is a professor of computer science at Stanford University(born 1939).He is the author of the “The Mathematical Theory of Computation”.It is published by McGraw Hill,1974;reprinted Dover,2003).It is one of the first texts to provide the mathematical concepts behind computer programming.


 images (1)

                         With Amir Pnueli, he co-authored an unfinished trilogy of textbooks on temporal logic and verification of reactive systems: The Temporal Logic of Reactive and Concurrent Systems: Specification (Springer-Verlag, 1991), The Temporal Logic of Reactive and Concurrent Systems: Safety (Springer-Verlag, 1995) and The Temporal Logic of Reactive and Concurrent Systems: Progress (unpublished).




                            Research Interests

  • Automated deduction: decision procedures, theorem proving, automated-based techniques.
  • Semantics, specification, and verification of reactive, embedded, real-time, and hybrid systems.
  • Systematic development, automatic synthesis and control.
  • Temporal logic and its applications. Automatic and machine-supported verification systems. Static analysis.


         In 1994 he was inducted as a Fellow  of the Association for Computing Machinery. The Association for Computing Machinery (ACM) is a U.S.-based international learned society for computing. It was founded in 1947 and is the world’s largest and most prestigious scientific and educational computing society.



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 MethodsThis 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.
    • group