Zohar Manna

On-line papers (in reverse chronological order):

• Zohar Manna, Anca Browne, Henny B. Sipma and Tomás E. Uribe. Visual Abstractions for Temporal Verification. In AMAST'98, vol. 1548 of LNCS, pp. 28-41, Springer-Verlag, 1998.

• Zohar Manna, Michael A. Colón, Bernd Finkbeiner, Henny B. Sipma and Tomás E. Uribe. Abstraction and Modular Verification of Infinite-State Reactive Systems. To appear in RTSE'98, LNCS, Springer-Verlag, 1998.

• Zohar Manna and Henny Sipma. Deductive Verification of Hybrid Systems using STeP. In Hybrid Systems: Computation and Control, vol. 1386 of LNCS, Springer-Verlag, 1998.

• Yonit Kesten, Zohar Manna and Amir Pnueli. Verification of Clocked and Hybrid Systems. In Embedded Systems, LNCS, Springer-Verlag, 1998.

• Zohar Manna and the STeP group. An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. To appear in TOOLS'98, LNCS, Springer-Verlag, 1998.

• Bernd Finkbeiner, Zohar Manna and Henny Sipma. Deductive Verification of Modular Systems. In Compositionality: The Significant Difference, COMPOS'97, vol. 1536 of LNCS, pp. 239-275, Springer-Verlag, 1998,

• Nikolaj Bjørner, Uri Lerner, and Zohar Manna. Deductive Verification of Parameterized Fault-Tolerant Systems: A Case Study. In Proc. of International Conference on Temporal Logic, Kluwer, July 1997. To appear.

• Nikolaj Bjørner, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Deductive Verification of Real-Time Systems Using STeP. In Proc. of ARTS'97, vol. 1231 of LNCS, pp. 22-43, Springer-Verlag, May 1997.

• Luca de Alfaro, Zohar Manna, Henny B. Sipma, and Tomás E. Uribe. Visual Verification of Reactive Systems. In Proc. of TACAS'97, vol. 1217 of LNCS, pp. 334-350, Springer Verlag, 1997.

• Luca de Alfaro, Arjun Kapur and Zohar Manna. Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification. In Proc. of 14th Symposium on Theoretical Aspects of Computer Science, vol. 1200 of Lecture Notes in Computer Science, pp. 153-164, Springer Verlag, Feb. 1997.

• Anca Browne, Zohar Manna and Henny B. Sipma. Hierarchical Verification using Verification Diagrams. In Second Asian Computing Science Conf., LNCS vol. 1179, pp. 276-286, December 1996.

• Zohar Manna and the STeP group. STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 415-418, Springer-Verlag, July 1996.

• Luca de Alfaro and Zohar Manna. Temporal Verification by Diagram Transformations. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 287-299, Springer-Verlag, July 1996.

• Henny B. Sipma, Tomás E. Uribe and Zohar Manna. Deductive Model Checking. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 209-219, Springer-Verlag, July 1996.

• Anca Browne, Luca de Alfaro, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Diagram-Based Formalisms for the Verification of Reactive Systems, in CADE-13 Workshop on Visual Reasoning, New Brunswick, NJ, July 1996.

• Yonit Kesten, Zohar Manna and Amir Pnueli. Verifying Clocked Transition Systems. In Hybrid Systems III, LNCS vol. 1066, pp. 13-40, Springer-Verlag, 1996.

• Zohar Manna and Amir Pnueli. Clocked Transition Systems. A tribute to Prof. C.S. Tang on his 70th birthday. Stanford CSD Technical Report STAN-CS-TR-96-1566. In Logic and Software Engineering, pp. 3-42, World Scientific Pub., 1996.

• I. Anca Browne, Zohar Manna and Henny Sipma. Generalized Temporal Verification Diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, vol. 1026 of LNCS, pp. 484-498, Bangalore, India, December 1995.

• Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover (Educational Release), User's Manual. Technical report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995.

• Nikolaj Bjørner, I. Anca Browne and Zohar Manna. Automatic Generation of Invariants and Intermediate Assertions. Theoretical Computer Science, vol. 173(1), pp. 49-87, February 1997. Original version appeared in 1st International Conference on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science 976, Cassis, France, pp. 589-623, September 1995.

• Anuchit Anuchitanukul, Zohar Manna and Tomás E. Uribe. Differential BDDs. In J. van Leeuwen, ed, Computer Science Today , Lecture Notes in Computer Science, Vol. 1000, pp. 218-233, Springer-Verlag, Sep. 1995.

• Luca de Alfaro and Zohar Manna, Verification in Continuous Time by Discrete Reasoning, 4th International Conference on Algebraic Methodology and Software Technology (AMAST), Montreal, Canada, pp. 292-306, July 1995.

• Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover (2-page abstract). In TAPSOFT'95: Theory and Practice of Software Development, Lecture Notes in Computer Science 915, pp. 793-794, May 1995.

• Edward Chang, Zohar Manna and Amir Pnueli. Compositional Verification of Real-time Systems. In IEEE Symposium on Logic in Computer Science, pp. 458-465, Paris, 1994.

• Arjun Kapur, Thomas A. Henzinger, Zohar Manna and Amir Pnueli. Proving Safety Properties of Hybrid Systems. International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Lecture Notes in Computer Science 863, pp. 431-454, Springer-Verlag, 1994.

• Henny B. Sipma and Zohar Manna, Specification and Verification of Controlled Systems, International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Lecture Notes in Computer Science 863, pp. 641-659, Springer-Verlag, 1994.

• Thomas A. Henzinger, Zohar Manna and Amir Pnueli. Temporal Proof Methodologies for Timed Transition Systems. Information and Computation, Vol. 112, No. 2, 1994, pp. 273-337.
  A shorter version appeared in the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 353-366, Orlando, Florida, January 1991.

• Yonit Kesten, Zohar Manna and Amir Pnueli. Temporal Verification of Simulation and Refinement. In REX Symposium A Decade of Concurrency, Lecture Notes in Computer Science 803, pp. 273-346, Springer-Verlag, 1994.

• Hugh McGuire, Zohar Manna and Richard Waldinger, Annotation-Based Deduction in Temporal Logic. First International Conference on Temporal Logic, Lecture Notes in Computer Science 827, pp. 430-444, Springer-Verlag, 1994.

• Zohar Manna and the STeP group. STeP: The Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.

• Zohar Manna and Amir Pnueli. Verification of Parameterized Programs. In Specification and Validation Methods (E. Borger, ed.), Oxford University Press, pp. 167-230, 1994.

• Zohar Manna and Amir Pnueli. Temporal Verification Diagrams. In International Symposium on Theoretical Aspects of Computer Software, Lecture Notes in Computer Science 789, Springer-Verlag, pp. 726-765, 1994.

• Zohar Manna and Amir Pnueli. Models for Reactivity. Acta Informatica, Vol. 30, pp. 609-678, 1993.

• Thomas A. Henzinger, Zohar Manna and Amir Pnueli. Towards Refining Temporal Specifications into Hybrid Systems. In Hybrid Systems, Lecture Notes in Computer Science 736, Springer-Verlag, pp. 60-76, 1993.

• Yonit Kesten, Zohar Manna, Hugh McGuire and Amir Pnueli. A Decision Algorithm for Full Propositional Temporal Logic. In 5th Conference on Computer Aided Verification, Lecture Notes in Computer Science 697, Springer-Verlag, pp. 97-109, 1993.

• Zohar Manna and Amir Pnueli. Verifying Hybrid Systems. In Hybrid Systems, Lecture Notes in Computer Science 736, Springer-Verlag, pp. 4-35, 1993.

• Zohar Manna and Amir Pnueli. A Temporal Proof Methodology for Reactive Systems. in Program Design Calculi, NATO ASI Series, Series F: Computer and System Sciences, Springer-Verlag, Vol. 118, 1993.
  An extended version is also available.

• Edward Chang, Zohar Manna and Amir Pnueli. Characterization of Temporal Property Classes. In 19th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 623, Springer-Verlag, pp. 474-486, 1992.

• Thomas A. Henzinger, Zohar Manna and Amir Pnueli. Timed Transition Systems. In REX workshop Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, Springer-Verlag, pp. 226-251, 1992.

• Thomas A. Henzinger, Zohar Manna and Amir Pnueli. What Good are Digital Clocks? In 19th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 623, Springer-Verlag, pp. 545-558, 1992.

• Oded Maler, Zohar Manna and Amir Pnueli. From Timed to Hybrid Systems. In REX workshop Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, Springer-Verlag, pp. 447-484, 1992.

• Zohar Manna and Amir Pnueli. Time for Concurrency. In 25th Anniversary of INRIA, Lecture Notes in Computer Science 653, Springer-Verlag, pp. 129-153, 1992.

• Zohar Manna and Richard Waldinger. Fundamentals of Deductive Program Synthesis. In Logic, Algebra, and Computation (F.L. Bauer, ed.), NATO Advanced Science Institutes Series, subseries F: Computer and System Sciences, Vol. 79, Springer-Verlag, 1991, pp. 41-107. Also in IEEE Transactions on Software Engineering, Vol. 18, No. 8 (August 1992), pp. 674-704.

• Edward Chang, Zohar Manna and Amir Pnueli. The Safety-Progress Classification. In Logic and Algebra of Specifications (F.L. Bauer, W. Brauer, and H. Schwichtenberg, eds.), NATO Advanced Science Institutes Series, Springer-Verlag, pp. 143-202, 1991.

• Zohar Manna and Amir Pnueli. Tools and Rules for the Practicing Verifier . In CMU Computer Science: A 25th Anniversary Commemorative, (R.F. Rashid, ed.), ACM Press and Addison-Wesley, pp. 125-159, 1991.

• Zohar Manna and Amir Pnueli. On the Faithfulness of Formal Models. In Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 520, Springer-Verlag, pp. 28-42, 1991.

• Zohar Manna and Amir Pnueli. An Exercise in the Verification of Multi-Process Programs. In Beauty is Our Business (W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, J. Misra, eds.), Springer-Verlag, pp. 289-301, 1990.

• Zohar Manna and Amir Pnueli. A Hierarchy of Temporal Properties. In 9th Symposium on Principles of Distributed Computing, Quebec, Canada, pp. 377-408, Aug. 1990.

• Zohar Manna and Amir Pnueli. Completing the Temporal Picture. In Theoretical Computer Science Journal, Vol. 83, No. 1, 1991, pp. 97-130. Also in 16th International Colloquium on Automata, Languages, and Programming, Springer-Verlag, Berlin, pp. 534-558, 1989.

• Zohar Manna and Amir Pnueli. The Anchored Version of the Temporal Framework. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science 354, Springer-Verlag, Berlin, pp. 201-284, 1989.

A number of other technical reports can be found at the Stanford Digital Library.

The Stanford home page.

The Computer Science Department home page.

The Theory Division home page.