Selected Publications

2008

  • M.Slanina, H.Sipma, Z.Manna, Deductive Verification of Alternating Systems. J. Formal Aspects of Computing, pp. 507-560 Vol 20, July 2008.

    • 2007

  • A. Bradley, Z. Manna, Checking Safety by Inductive Generalization of Counterexamples to Induction. Formal Methods in Computer-Aided Design (FMCAD), Vol. 7, 2007

  • Z. Manna, H. Sipma, T. Zhang, Verifying Balanced Trees. In Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS), Lecture Notes in Computer Science, vol. 4514, pp. 363-378, Springer-Verlag, 2007.

  • Cesar Sanchez, Henny B. Sipma and Zohar Manna A Family of Distributed Deadlock Avoidance Protocols and their reachable State Spaces, In Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering (FASE'07). colocated with ETAPS'07, vol. 4422 of Lecture Notes in Computer Science (LNCS), pp. 155-169, Springer-Verlag, 2007.

  • Cesar Sanchez, Henny B. Sipma and Zohar Manna Generating Efficient Distributed Deadlock Avoidance Controllers, In The Fifteenth International Workshop on Parallel and Distributed Real-Time Systems (WPDRTS 2007). collocated with IPDPS'07 (21st IEEE International Parallel and Distributed Processing Symposium), IEEE Computer Society Press, 2007.

    • 2006

  • Cesar Sanchez, Henny B. Sipma, Christopher Gill, Zohar Manna, Distributed Priority Inheritance for Real-Time and Embedded Systems. In Proc. 10th International Conference on Principles of Distributed Systems (OPODIS), Lecture Notes in Computer Science 4305, Springer-Verlag, 2006, pp. 110-125.

  • Matteo Slanina, Henny B. Sipma, and Zohar Manna, Proving ATL* Properties of Infinite-State Systems. In Proc. International Colloquium on Theoretical Aspects of Computing (ICTAC 2006), Lecture Notes in Computer Science, Vol. 4281, Springer Verlag, 2006.

  • Aaron R. Bradley and Zohar Manna, Verification Constraint Problems with Strengthening. In Proc. International Colloquium on Theoretical Aspects of Computing (ICTAC 2006), Lecture Notes in Computer Science, Vol. 4281, Springer Verlag, 2006.

  • Cesar Sanchez, Henny B. Sipma, Zohar Manna, Christopher D. Gill, Efficient Distributed Deadlock Avoidance with Liveness Guarantees. In Proceedings of the 6th ACM & IEEE Conference on Embedded Software (EMSOFT'06), pp. 12-20, ACM Press, 2006.

  • Ting Zhang, Henny B. Sipma, Zohar Manna, Decision procedures for term algebras with integer constraints, In Information and Computation, volume 204, pp 1526-1574, October 2006.

  • Cesar Sanchez, Henny B. Sipma, Zohar Manna, Venkita Subramonian, and Christopher D. Gill, On Efficient Distributed Deadlock Avoidance for Distributed Real-Time and Embedded Systems, In Proc. of the 20th IEEE Int'l Parallel and Distributed Processing Symposium (IPDPS'06), IEEE Computer Society Press, 2006.

  • Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Fixed point iteration for computing the time elapse operator, In Proc. Hybrid Systems: Computation and Control (HSCC 2006), Lecture Notes in Computer Science. Vol. 3927, Springer Verlag, 2006.

  • Aaron R. Bradley, Henny Sipma, and Zohar Manna, What's Decidable About Arrays?, In Proc. Verification, Model-Checking, and Abstract-Interpretation (VMCAI), LNCS, Vol. 3855, Springer Verlag, 2006 January 2006.

  • Sriram Sankaranarayanan, Michael Colon Henny Sipma, Zohar Manna, Efficient Strongly Relational Polyhedral Analysis, In Proc. Verification, Model-Checking, and Abstract Interpretation (VMCAI), LNCS, Vol. 3855, Springer Verlag, 2006.

    • 2005

  • Ting Zhang, Henny B. Sipma, Zohar Manna, Decision Procedures for Queues with Integer Constraints, In Proc. Foundations of Software Technology and Theoretical Computer Science (FSTTCS) December 2005, Lecture Notes in Computer Science, Volume 3821, Springer-Verlag.

  • Cesar Sanchez, Henny B. Sipma, Venkita Subramonian, Christopher Gill, Zohar Manna, Thread Allocation Protocols for Distributed Real-Time and Embedded Systems. In Proc. Formal Techniques for Networked and Distributed Systems (FORTE) October 2005, Lecture Notes in Computer Science, Volume 3731, Springer-Verlag.

  • Cesar Sanchez, Matteo Slanina, Henny B. Sipma, Zohar Manna, Expressive Completeness of an Event-Pattern Reactive Programming Language. In Proc. Formal Techniques for Networked and Distributed Systems (FORTE) October 2005, Lecture Notes in Computer Science, Volume 3731, Springer-Verlag.

  • Cesar Sanchez, Henny B. Sipma, Matteo Slanina, Zohar Manna, Final Semantics for Event-Pattern Reactive Programs, In Proc. Conference on Algebra and Coalgebra in Computer Science (CALCO) September 2005, Lecture Notes in Computer Science, Volume 3629, Springer-Verlag.

  • Aaron R. Bradley, Henny Sipma, and Zohar Manna, Termination Analysis of Integer Linear Loops, In Proc. Concurrency Theory (CONCUR) August 2005, Lecture Notes In Computer Science, Volume 3653, Springer-Verlag.

  • Ting Zhang, Henny B. Sipma, Zohar Manna, The Decidability of the First-order Theory of Knuth-Bendix Order, In Proc. Conference on Automated Deduction (CADE) July 2005, Lecture Notes in Computer Science, Volume 3632, Springer-Verlag.

  • Aaron R. Bradley, Henny Sipma, and Zohar Manna, The Polyranking Principle, In Proc. Automata, Languages and Programming (ICALP) July 2005, Lecture Notes in Computer Science, Volume 3580, Springer-Verlag.

  • Aaron R. Bradley, Henny Sipma, and Zohar Manna, Linear Ranking with Reachability, In Proc. Computer-Aided Verification (CAV) July 2005, Lecture Notes in Computer Science, Volume 3576, Springer-Verlag.

  • Ben d'Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna, LOLA: Runtime Monitoring of Synchronous Systems, In Proc. of the 12th International Symposium of Temporal Representation and Reasoning (TIME 2005), pp. 166-174, IEEE Computer Society Press, 2005.

  • Aaron R. Bradley, Henny Sipma, and Zohar Manna, Termination of Polynomial Programs, In Proc. Verification, Model-Checking, and Abstract-Interpretation (VMCAI) January 2005, Lecture Notes in Computer Science, Volume 3385, Springer-Verlag.

  • Sriram Sankaranarayanan, Henny Sipma, Zohar Manna, Scalable Analysis of Linear Systems using Mathematical Programming, In Proc. Verification, Model-Checking, and Abstract Interpretation (VMCAI) January 2005, Lecture Notes in Computer Science, Volume 3385, Springer-Verlag.

    • 2004

  • Ting Zhang, Henny B. Sipma and Zohar Manna, Term Algebras with Length Function and Bounded Quantifier Alternation, In Proc. 17th International Conference on Theorem Proving in Higher Order Logics (TPHOL), Lecture Notes in Computer Science 3223, Springer-Verlag, 2004, pp. 321-336.

  • Sriram Sankaranarayanan, Henny B. Sipma and Zohar Manna, Constraint-based Linear Relations Analysis, In Proc. 11th Static Analysis Symposium (SAS'2004), Vol 3148 of Lecture Notes in Computer Science, Springer Verlag, pp 53-68, August 2004.

  • Ting Zhang and Henny Sipma and Zohar Manna, Decision Procedures for Recursive Data Structures with Integer Constraints, In Proc. 2nd International Joint Conference on Automated Reasoning (IJCAR'04), Vol 3097 of Lecture Notes in Computer Science, Springer Verlag, pp 152-167, July 2004. (Best Paper Award)

  • Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna, Constructing Invariants for Hybrid Systems, In Hybrid Systems: Computation and Control (HSCC 2004), Lecture Notes in Computer Science, Volume 2993, pp. 539-554 (March 2004)

  • Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna, Non-Linear Loop Invariant Generation using Grobner Bases, in ACM Principles of Programming Languages (POPL 2004). pp. 318-329 (January 2004)

    • 2003

  • Zohar Manna and Calogero Zarba. Combining Decision Procedures. In Formal Methods at the Crossroads: from Panacea to Foundational Support, Lecture Notes in Computer Science, Volume 2787, Springer-Verlag, November 2003, pp. 381-422.

  • Cesar Sánchez, Sriram Sankaranarayanan, Henny B. Sipma, Ting Zhang, David Dill, and Zohar Manna, Event Correlation: Language and Semantics. In Embedded Software (EMSOFT 2003), Lecture Notes in Computer Science (LNCS) 2855, Springer-Verlag, pp. 323-339, 2003.

  • Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna, Petri-Net Analysis using Invariant Generation, In Verification: Theory and Practice, Lecture Notes in Computer Science(LNCS) 2772 (Invited Paper).

  • Calogero G. Zarba, Zohar Manna, and Henny B. Sipma, Combining theories sharing dense orders, In Automated Reasoning with Analytic Tableaux and Related Methods: Position Papers and Tutorials (2003).

    • 2001

  • Nikolaj Bjorner, Zohar Manna, Henny Sipma and Tomas Uribe. Deductive Verification of Real-time Systems using STeP. Theoretical Computer Science, (253) 2001, pp 27-60.

    • 2000

  • Zohar Manna, Henny Sipma, Alternating the Temporal Picture for Safety. In Proc. 27th Intl. Colloq. Aut. Lang. Prog.(ICALP 2000). LNCS 1853, Springer-Verlag, pp 429-450.

  • Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomas Uribe. Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. In Formal Methods in System Design, vol 16, pp 227-270.

    • 1999

  • Zohar Manna and Henny Sipma, Verification of Parameterized Systems by Dynamic Induction on Diagrams, CAV'99, pp 25-43, LNCS 1633, Springer-Verlag, 1999.

  • Henny B. Sipma, Tomas E. Uribe and Zohar Manna. Deductive Model Checking. Formal Methods in System Design, Vol 15, pp 49-74 (1999).

  • Zohar Manna, Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma, Tomas Uribe. An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. In Tool Support for System Specification, Development and Verification, Advances in Computing Science, pp 174-188, Springer Verlag, 1999.

    • 1998

  • Zohar Manna and Henny Sipma. Deductive Verification of Hybrid Systems using STeP. In Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 1386, Springer-Verlag, 1998.

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

  • Zohar Manna, Anca Browne, Henny Sipma, and Tomas Uribe. Visual Abstraction for Temporal Verification. In AMAST'98, Vol 1548 of LNCS, pp 28-41, Springer-Verlag, 1998.

  • Zohar Manna, Michael Colon, Bernd Finkbeiner, Henny Sipma, and Tomas Uribe. Abstraction and Modular Verification of Infinite-State Reactive Systems. Requirements Targeting Software and Systems Engineering (RTSE), LNCS 1526, Springer Verlag, pp 273-292, 1998.

  • Luca de Alfaro, Zohar Manna and Henny B. Sipma. Decomposing, Transforming and Composing Diagrams: The joys of Modular Verification, Technical Report STAN-CS-98-1614, Stanford University, 1998.

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

    1997

  • Nikolaj Bjorner, 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.

  • Nikolaj Bjorner, 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.

  • Nikolaj Bjorner, Zohar Manna, Henny B. Sipma and Tomas 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 Tomas 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.

    • 1996

  • 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, Tomas 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 Tomas 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.

    • 1995

  • 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 Bjorner, 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 Tomas 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.

    • 1994

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

    • 1993

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

    • 1992

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

    • 1991

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

  • Zohar Manna and Amir Pnueli. Temporal Specification and Verification of Reactive Modules. Weizmann Institute of Science Technical Report, March 1992.

    1991

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

    • 1990

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

    • 1989

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

    Papers published by the STeP group can be accessed here.
    Many of my older papers can be accessed through my DBLP entry.
    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