| 2007 | FASE | A Family of Distributed Deadlock Avoidance Protocols and Their Reachable State Spaces. | Csar Snchez, Henny B. Sipma, Zohar Manna |
| 2007 | FMCAD | Checking Safety by Inductive Generalization of Counterexamples to Induction. | Aaron R. Bradley, Zohar Manna |
| 2007 | LFCS | Verifying Balanced Trees. | Zohar Manna, Henny B. Sipma, Ting Zhang |
| 2006 | EMSOFT | Efficient distributed deadlock avoidance with liveness guarantees. | Csar Snchez, Henny B. Sipma, Zohar Manna, Christopher D. Gill |
| 2006 | ICTAC | Verification Constraint Problems with Strengthening. | Aaron R. Bradley, Zohar Manna |
| 2006 | ICTAC | Proving ATL* Properties of Infinite-State Systems. | Matteo Slanina, Henny B. Sipma, Zohar Manna |
| 2006 | OPODIS | Distributed Priority Inheritance for Real-Time and Embedded Systems. | Csar Snchez, Henny B. Sipma, Christopher D. Gill, Zohar Manna |
| 2006 | VMCAI | What's Decidable About Arrays? | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2006 | VMCAI | Efficient Strongly Relational Polyhedral Analysis. | Sriram Sankaranarayanan, Michael Coln, Henny B. Sipma, Zohar Manna |
| 2005 | ATVA | Termination and Invariance Analysis of Loops. | Aaron R. Bradley, Zohar Manna |
| 2005 | CADE | The Decidability of the First-Order Theory of Knuth-Bendix Order. | Ting Zhang, Henny B. Sipma, Zohar Manna |
| 2005 | CALCO | Final Semantics for Event-Pattern Reactive Programs. | Csar Snchez, Henny B. Sipma, Matteo Slanina, Zohar Manna |
| 2005 | CAV | Linear Ranking with Reachability. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | CONCUR | Termination Analysis of Integer Linear Loops. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | FORTE | Thread Allocation Protocols for Distributed Real-Time and Embedded Systems. | Csar Snchez, Henny B. Sipma, Venkita Subramonian, Christopher D. Gill, Zohar Manna |
| 2005 | FORTE | Expressive Completeness of an Event-Pattern Reactive Programming Language. | Csar Snchez, Matteo Slanina, Henny B. Sipma, Zohar Manna |
| 2005 | ICALP | The Polyranking Principle. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | TIME | LOLA: Runtime Monitoring of Synchronous Systems. | Ben D'Angelo, Sriram Sankaranarayanan, Csar Snchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna |
| 2005 | VMCAI | Termination of Polynomial Programs. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | VMCAI | Scalable Analysis of Linear Systems Using Mathematical Programming. | Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna |
| 2004 | CADE | Decision Procedures for Recursive Data Structures with Integer Constraints. | Ting Zhang, Henny B. Sipma, Zohar Manna |
| 2004 | POPL | Non-linear loop invariant generation using Gröbner bases. | Sriram Sankaranarayanan, Henny Sipma, Zohar Manna |
| 2004 | SAS | Constraint-Based Linear-Relations Analysis. | Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna |
| 2003 | EMSOFT | Event Correlation: Language and Semantics. | Csar Snchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David L. Dill, Zohar Manna |
| 2000 | ICALP | Alternating the Temporal Picture for Safety. | Zohar Manna, Henny Sipma |
| 1999 | CAV | Verification of Parameterized Systems by Dynamic Induction on Diagrams. | Zohar Manna, Henny Sipma |
| 1999 | TIME | Visual Verification of Temporal Properties. | Zohar Manna |
| 1997 | STACS | Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification. | Luca de Alfaro, Arjun Kapur, Zohar Manna |
| 1997 | TACAS | Visual Verification of Reactive Systems. | Luca de Alfaro, Zohar Manna, Henny B. Sipma, Toms E. Uribe |
| 1996 | CAV | Temporal Verification by Diagram Transformations. | Luca de Alfaro, Zohar Manna |
| 1996 | CAV | STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. | Nikolaj S. Bjrner, Anca Browne, Edward Y. Chang, Michael Coln, Arjun Kapur, Zohar Manna, Henny Sipma, Toms E. Uribe |
| 1996 | CAV | Deductive Model Checking. | Henny Sipma, Toms E. Uribe, Zohar Manna |
| 1995 | CP | Automatic Generation of Invariants and Assertions. | Nikolaj S. Bjrner, Anca Browne, Zohar Manna |
| 1994 | CAV | Realizability and Synthesis of Reactive Modules. | Anuchit Anuchitanukul, Zohar Manna |
| 1994 | CAV | Beyond Model Checking. | Zohar Manna |
| 1994 | LICS | Compositional Verification of Real-Time Systems | Edward Y. Chang, Zohar Manna, Amir Pnueli |
| 1993 | CAV | A Decision Algorithm for Full Propositional Temporal Logic. | Yonit Kesten, Zohar Manna, Hugh McGuire, Amir Pnueli |
| 1992 | CADE | The Special-Relation Rules are Incomplete. | Zohar Manna, Richard J. Waldinger |
| 1992 | ICALP | Characterization of Temporal Property Classes. | Edward Y. Chang, Zohar Manna, Amir Pnueli |
| 1992 | ICALP | What Good Are Digital Clocks? | Thomas A. Henzinger, Zohar Manna, Amir Pnueli |
| 1991 | MFCS | On the Faithfulness of Formal Models. | Zohar Manna, Amir Pnueli |
| 1991 | POPL | Temporal Proof Methodologies for Real-time Systems. | Thomas A. Henzinger, Zohar Manna, Amir Pnueli |
| 1990 | PODC | A Hierarchy of Temporal Properties. | Zohar Manna, Amir Pnueli |
| 1989 | ICALP | Completing the Temporal Picture. | Zohar Manna, Amir Pnueli |
| 1987 | AAAI | The Deductive Synthesis of Imperative LISP Programs. | Zohar Manna, Richard J. Waldinger |
| 1987 | PODC | A Hierarchy of Temporal Properties (Abstract). | Zohar Manna, Amir Pnueli |
| 1987 | POPL | Specification and Verification of Concurrent Programs By Forall-Automata. | Zohar Manna, Amir Pnueli |
| 1986 | CADE | Modal Theorem Proving. | Martn Abadi, Zohar Manna |
| 1986 | CADE | How to Clear a Block: Plan Formation in Situational Logic. | Zohar Manna, Richard J. Waldinger |
| 1986 | LICS | A Timely Resolution | Martn Abadi, Zohar Manna |
| 1986 | LICS | Towards Deductive Synthesis of Dataflow Networks | Bengt Jonsson, Zohar Manna, Richard J. Waldinger |
| 1985 | ICALP | Special Relations in Automated Deduction. | Zohar Manna, Richard J. Waldinger |
| 1985 | IJCAI | The Origin of the Binary-Search Paradigm. | Zohar Manna, Richard J. Waldinger |
| 1983 | ICALP | A Hardware Semantics Based on Temporal Intervals. | Joseph Y. Halpern, Zohar Manna, Ben C. Moszkowski |
| 1983 | ICALP | Proving Precedence Properties: The Temporal Way. | Zohar Manna, Amir Pnueli |
| 1983 | POPL | How to Cook a Temporal Proof System for Your Pet Language. | Zohar Manna, Amir Pnueli |
| 1981 | POPL | The Temporal Logic of Branching Time. | Mordechai Ben-Ari, Zohar Manna, Amir Pnueli |
| 1980 | POPL | Synchronous Schemes and Their Decision Problems. | Zohar Manna, Amir Pnueli |
| 1979 | ICALP | Proving termination with Multiset Orderings. | Nachum Dershowitz, Zohar Manna |
| 1979 | ICALP | The Modal Logic of Programs. | Zohar Manna, Amir Pnueli |
| 1979 | IJCAI | A Deductive Approach to Program Synthesis. | Zohar Manna, Richard Waldinger |
| 1978 | ICSE | Inference Rules for Program Annotation. | Nachum Dershowitz, Zohar Manna |
| 1978 | ICSE | The Synthesis of Structure Changing Programs. | Zohar Manna, Richard J. Waldinger |
| 1977 | IJCAI | The Automatic Synthesis of Systems of Recursive Programs. | Zohar Manna, Richard J. Waldinger |
| 1977 | POPL | The Evolution of Programs: A System for Automatic Program Modification. | Nachum Dershowitz, Zohar Manna |
| 1976 | ICSE | Is 'Sometime' Sometimes Better Than 'Always'? Intermittent Assertions in Proving Program Correctness. | Zohar Manna, Richard J. Waldinger |
| 1975 | IJCAI | Knowledge and Reasoning in Program Synthesis. | Richard J. Waldinger, Zohar Manna |
| 1975 | STOC | The Optimal Fixedpoint of Recursive Programs | Zohar Manna, Adi Shamir |
| 1973 | IJCAI | A Heuristic Approach to Program Verification. | Shmuel Katz, Zohar Manna |
| 1972 | ICALP | Fixpoint Approach to the Theory of Computation. | Zohar Manna, Jean Vuillemin |
| 1972 | STOC | Program Schemas with Equality | Ashok K. Chandra, Zohar Manna |
| 1970 | STOC | Second-Order Mathematical Theory of Computation | Zohar Manna |
| 1969 | STOC | Formalization of Properties of Recursively Defined Functions | Zohar Manna, Amir Pnueli |