Formalization of Properties of Recursively Defined Functions - Zohar Manna; Amir Pnueli (STOC, 1969)

Properties of Programs and the First-Order Predicate Calculus. - Zohar Manna (J. ACM, 1969)

The Correctness of Programs. - Zohar Manna (J. Comput. Syst. Sci., 1969)

Termination of programs represented as interpreted graphs. - Zohar Manna (AFIPS Spring Joint Computing Conference, 1970)

Second-Order Mathematical Theory of Computation - Zohar Manna (STOC, 1970)

The Correctness of Nondeterministic Programs. - Zohar Manna (Artif. Intell., 1970)

Formalization of Properties of Functional Programs. - Zohar Manna; Amir Pnueli (J. ACM, 1970)

The Translation of 'Go To' Programs to 'While' Programs. - Edward A. Ashcroft; Zohar Manna (IFIP Congress (1), 1971)

Toward Automatic Program Synthesis. - Zohar Manna; Richard J. Waldinger (Commun. ACM, 1971)

Mathematical Theory of Partial Correctness. - Zohar Manna (J. Comput. Syst. Sci., 1971)

Mathematical theory of partial correctness. - Zohar Manna (Symposium on Semantics of Algorithmic Languages, 1971)

Towards automatic program synthesis. - Zohar Manna; Richard J. Waldinger (Symposium on Semantics of Algorithmic Languages, 1971)

Computation of recursive programs: theory vs practice. - Zohar Manna (AFIPS Spring Joint Computing Conference, 1972)

Fixpoint Approach to the Theory of Computation. - Zohar Manna; Jean Vuillemin (ICALP, 1972)

Recursive definitions of partial functions and their computations. - Jean-Marie Cadiou; Zohar Manna (Proving Assertions About Programs, 1972)

Program Schemas with Equality - Ashok K. Chandra; Zohar Manna (STOC, 1972)

Fix Point Approach to the Theory of Computation. - Zohar Manna; Jean Vuillemin (Commun. ACM, 1972)

A Heuristic Approach to Program Verification. - Shmuel Katz; Zohar Manna (IJCAI, 1973)

Inductive Methods for Proving Properties of Programs. - Zohar Manna; Stephen Nes; Jean Vuillemin (Commun. ACM, 1973)

Decidable Properties of Monadic Functional Schemas. - Edward A. Ashcroft; Zohar Manna; Amir Pnueli (J. ACM, 1973)

Knowledge and Reasoning in Program Synthesis. - Zohar Manna (Programming Methodology, 1974)

Axiomatic Approach to Total Correctness of Programs. - Zohar Manna; Amir Pnueli (Acta Informatica, 1974)

Towards automatic debugging of programs. - Shmuel Katz; Zohar Manna (Reliable Software, 1975)

The Optimal Fixedpoint of Recursive Programs - Zohar Manna; Adi Shamir (STOC, 1975)

A Closer Look at Termination. - Shmuel Katz; Zohar Manna (Acta Informatica, 1975)

Knowledge and Reasoning in Program Synthesis. - Zohar Manna; Richard J. Waldinger (Artif. Intell., 1975)

Translating Program Schemas to While-Schemas. - Edward A. Ashcroft; Zohar Manna (SIAM J. Comput., 1975)

Logical Analysis of Programs. - Shmuel Katz; Zohar Manna (Commun. ACM, 1976)

On the Power of Programming Features. - Ashok K. Chandra; Zohar Manna (Comput. Lang., 1976)

The Theoretical Aspects of the Optimal Fixed Point. - Zohar Manna; Adi Shamir (SIAM J. Comput., 1976)

The Automatic Synthesis of Systems of Recursive Programs. - Zohar Manna; Richard J. Waldinger (IJCAI, 1977)

The Evolution of Programs: A System for Automatic Program Modification. - Nachum Dershowitz; Zohar Manna (POPL, 1977)

The Optimal Approach to Recursive Programs. - Zohar Manna; Adi Shamir (Commun. ACM, 1977)

The automatic synthesis of recursive programs. - Zohar Manna; Richard Waldinger (Artificial Intelligence and Programming Languages, 1977)

The Evolution of Programs: Automatic Program Modification. - Nachum Dershowitz; Zohar Manna (IEEE Trans. Software Eng., 1977)

DEDALUS - The DEDuctive ALgorithm Ur-Synthesizer. - Zohar Manna; Richard Waldinger (AFIPS National Computer Conference, 1978)

The Synthesis of Structure Changing Programs. - Zohar Manna; Richard J. Waldinger (ICSE, 1978)

Is "Sometime" Sometimes Better Than "Always"? (Intermittent Assertions in Proving Program Correctness). - Zohar Manna; Richard J. Waldinger (Commun. ACM, 1978)

The Convergence of Functions to Fixedpoints of Recursive Definitions. - Zohar Manna; Adi Shamir (Theor. Comput. Sci., 1978)

The Logic of Computer Programming. - Zohar Manna; Richard J. Waldinger (IEEE Trans. Software Eng., 1978)

The Modal Logic of Programs. - Zohar Manna; Amir Pnueli (ICALP, 1979)

Proving Termination with Multiset Orderings. - Nachum Dershowitz; Zohar Manna (Commun. ACM, 1979)

Synthesis: Dreams - Programs. - Zohar Manna; Richard J. Waldinger (IEEE Trans. Software Eng., 1979)

Logics of Programs. - Zohar Manna (IFIP Congress, 1980)

Synchronous Schemes and Their Decision Problems. - Zohar Manna; Amir Pnueli (POPL, 1980)

A Deductive Approach to Program Synthesis. - Zohar Manna; Richard J. Waldinger (ACM Trans. Program. Lang. Syst., 1980)

Verification of Concurrent Programs: Temporal Proof Principles. - Zohar Manna; Amir Pnueli (Logic of Programs, 1981)

Problematic Features of Programming Languages: A Situational-Calculus Approach. - Zohar Manna; Richard J. Waldinger (Acta Informatica, 1981)

Deductive Synthesis of the Unification Algorithm. - Zohar Manna; Richard J. Waldinger (Sci. Comput. Program., 1981)

Inference Rules for Program Annotation. - Nachum Dershowitz; Zohar Manna (IEEE Trans. Software Eng., 1981)

A Hardware Semantics Based on Temporal Intervals. - Joseph Y. Halpern; Zohar Manna; Ben C. Moszkowski (ICALP, 1983)

Proving Precedence Properties: The Temporal Way. - Zohar Manna; Amir Pnueli (ICALP, 1983)

Reasoning in Interval Temporal Logic. - Ben C. Moszkowski; Zohar Manna (Logic of Programs, 1983)

How to Cook a Temporal Proof System for Your Pet Language. - Zohar Manna; Amir Pnueli (POPL, 1983)

The Temporal Logic of Branching Time. - Mordechai Ben-Ari; Amir Pnueli; Zohar Manna (Acta Informatica, 1983)

TABLOG: The Deductive-Tableau Programming Language. - Yonathan Malachi; Zohar Manna; Richard J. Waldinger (LISP and Functional Programming, 1984)

Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs. - Zohar Manna; Amir Pnueli (Sci. Comput. Program., 1984)

Synthesis of Communicating Processes from Temporal Logic Specifications. - Zohar Manna; Pierre Wolper (ACM Trans. Program. Lang. Syst., 1984)

Deduction with Relation Matching. - Zohar Manna; Richard J. Waldinger (FSTTCS, 1985)

Nonclausal Temporal Deduction. - Martín Abadi; Zohar Manna (Logic of Programs, 1985)

TABLOG: A New Approach To Logic Programming. - Yonathan Malachi; Zohar Manna; Richard J. Waldinger (Logic Programming: Functions, Relations, and Equations, 1986)

Modal Theorem Proving. - Martín Abadi; Zohar Manna (CADE, 1986)

How to Clear a Block: Plan Formation in Situational Logic. - Zohar Manna; Richard J. Waldinger (CADE, 1986)

A Timely Resolution - Martín Abadi; Zohar Manna (LICS, 1986)

Towards Deductive Synthesis of Dataflow Networks - Bengt Jonsson 001; Zohar Manna; Richard J. Waldinger (LICS, 1986)

Special relations in automated deduction. - Zohar Manna; Richard J. Waldinger (J. ACM, 1986)

Tablog: Functional and Relational Programming in One Framework. - Yonathan Malachi; Zohar Manna; Richard J. Waldinger (IEEE Softw., 1986)

The Deductive Synthesis of Imperative LISP Programs. - Zohar Manna; Richard J. Waldinger (AAAI, 1987)

A Hierarchy of Temporal Properties (Abstract). - Zohar Manna; Amir Pnueli (PODC, 1987)

Specification and Verification of Concurrent Programs by forall-Automata. - Zohar Manna; Amir Pnueli (Temporal Logic in Specification, 1987)

How to Clear a Block: A Theory of Plans. - Zohar Manna; Richard J. Waldinger (J. Autom. Reason., 1987)

The Origin of a Binary-Search Paradigm. - Zohar Manna; Richard J. Waldinger (Sci. Comput. Program., 1987)

The anchored version of the temporal framework. - Zohar Manna; Amir Pnueli (REX Workshop, 1988)

Temporal Logic Programming. - Martín Abadi; Zohar Manna (J. Symb. Comput., 1989)

An interleaving model for real-time. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (Jerusalem Conference on Information Technology, 1990)

A temporal proof methodology for reactive systems. - Zohar Manna; Amir Pnueli (Jerusalem Conference on Information Technology, 1990)

A Hierarchy of Temporal Properties. - Zohar Manna; Amir Pnueli (PODC, 1990)

Nonclausal Deduction in First-Order Temporal Logic - Martín Abadi; Zohar Manna (J. ACM, 1990)

Monotonicity Properties in Automated Deduction. - Zohar Manna; Mark E. Stickel; Richard Waldinger (Artificial and Mathematical Theory of Computation, 1991)

On the Faithfulness of Formal Models. - Zohar Manna; Amir Pnueli (MFCS, 1991)

Temporal Proof Methodologies for Real-time Systems. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (POPL, 1991)

Timed Transition Systems. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (REX Workshop, 1991)

From Timed to Hybrid Systems. - Oded Maler; Zohar Manna; Amir Pnueli (REX Workshop, 1991)

Completing the Temporal Picture. - Zohar Manna; Amir Pnueli (Theor. Comput. Sci., 1991)

The temporal logic of reactive and concurrent systems - specification. - Zohar Manna; Amir Pnueli (Springer, 1992)

The Special-Relation Rules are Incomplete. - Zohar Manna; Richard J. Waldinger (CADE, 1992)

Towards Refining Temporal Specifications into Hybrid Systems. - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (Hybrid Systems, 1992)

Verifying Hybrid Systems. - Zohar Manna; Amir Pnueli (Hybrid Systems, 1992)

Characterization of Temporal Property Classes. - Edward Y. Chang; Zohar Manna; Amir Pnueli (ICALP, 1992)

What Good Are Digital Clocks? - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (ICALP, 1992)

Time for Concurrency. - Zohar Manna; Amir Pnueli (25th Anniversary of INRIA, 1992)

Fundamentals of Deductive Program Synthesis. - Zohar Manna; Richard J. Waldinger (IEEE Trans. Software Eng., 1992)

The deductive foundations of computer programming - a one-volume version of "The logical basis for computer programming". - Zohar Manna; Richard J. Waldinger (Addison-Wesley, 1993)

Verification of parameterized programs. - Zohar Manna; Amir Pnueli (Specification and validation methods, 1993)

A Decision Algorithm for Full Propositional Temporal Logic. - Yonit Kesten; Zohar Manna; Hugh McGuire; Amir Pnueli (CAV, 1993)

Temporal Verification of Simulation and Refinement. - Yonit Kesten; Zohar Manna; Amir Pnueli (REX School/Symposium, 1993)

Models for Reactivity. - Zohar Manna; Amir Pnueli (Acta Informatica, 1993)

Realizability and Synthesis of Reactive Modules. - Anuchit Anuchitanukul; Zohar Manna (CAV, 1994)

Beyond Model Checking. - Zohar Manna (CAV, 1994)

Prooving Safety Properties of Hybrid Systems. - Arjun Kapur; Thomas A. Henzinger; Zohar Manna; Amir Pnueli (FTRTFT, 1994)

Specification and Verification of Controlled Systems. - Henny Sipma; Zohar Manna (FTRTFT, 1994)

Annotation-Based Deduction in Temporal Logic. - Hugh McGuire; Zohar Manna; Richard J. Waldinger (ICTL, 1994)

Compositional Verification of Real-Time Systems - Edward Y. Chang; Zohar Manna; Amir Pnueli (LICS, 1994)

Temporal Verification Diagrams. - Zohar Manna; Amir Pnueli (TACS, 1994)

Temporal Proof Methodologies for Timed Transition Systems - Thomas A. Henzinger; Zohar Manna; Amir Pnueli (Inf. Comput., 1994)

Temporal verification of reactive systems - safety. - Zohar Manna; Amir Pnueli (Springer, 1995)

Differential BDDs. - Anuchit Anuchitanukul; Zohar Manna; Tomás E. Uribe (Computer Science Today, 1995)

Verification in Continuous Time by Discrete Reasoning. - Luca de Alfaro; Zohar Manna (AMAST, 1995)

Automatic Generation of Invariants and Assertions. - Nikolaj S. Bjørner; Anca Browne; Zohar Manna (CP, 1995)

Generalized Temporal Verification Diagrams. - Anca Browne; Zohar Manna; Henny Sipma (FSTTCS, 1995)

Verifying Clocked Transition Systems. - Yonit Kesten; Zohar Manna; Amir Pnueli (Hybrid Systems, 1995)

STeP: The Stanford Temporal Prover. - Zohar Manna; Nikolaj S. Bjørner; Anca Browne; Edward Y. Chang; Michael Colón; Luca de Alfaro; Harish Devarajan; Arjun Kapur; Jaejin Lee; Henny Sipma; Tomás E. Uribe (TAPSOFT, 1995)

A Temporal Plan Theory. - Zohar Manna; Massimo Paltrinieri; Richard J. Waldinger (WOCFAI, 1995)

Hierarchical Verification Using Verification Diagrams. - Anca Browne; Zohar Manna; Henny Sipma (ASIAN, 1996)

Temporal Verification by Diagram Transformations. - Luca de Alfaro; Zohar Manna (CAV, 1996)

STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems. - Nikolaj S. Bjørner; Anca Browne; Edward Y. Chang; Michael Colón; Arjun Kapur; Zohar Manna; Henny Sipma; Tomás E. Uribe (CAV, 1996)

Verification of Progress Properties. - Zohar Manna (APPIA-GULP-PRODE, 1997)

Deductive Verification of Modular Systems. - Bernd Finkbeiner; Zohar Manna; Henny Sipma (COMPOS, 1997)

Abstraction and Modular Verification of Infinite-State Reactive Systems. - Zohar Manna; Michael Colón; Bernd Finkbeiner; Henny Sipma; Tomás E. Uribe (Requirements Targeting Software and Systems Engineering, 1997)

Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification. - Luca de Alfaro; Arjun Kapur; Zohar Manna (STACS, 1997)

Visual Verification of Reactive Systems. - Luca de Alfaro; Zohar Manna; Henny B. Sipma; Tomás E. Uribe (TACAS, 1997)

Automatic Generation of Invariants and Intermediate Assertions. - Nikolaj S. Bjørner; Anca Browne; Zohar Manna (Theor. Comput. Sci., 1997)

Visual Abstractions for Temporal Verification. - Zohar Manna; Anca Browne; Henny Sipma; Tomás E. Uribe (AMAST, 1998)

Deductive Verification of Hybrid Systems Using STeP. - Zohar Manna; Henny Sipma (HSCC, 1998)

An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. - Zohar Manna; Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Mark C. Pichora; Henny B. Sipma; Tomás E. Uribe (Tool Support for System Specification, Development and Verification, 1998)

Verification of Parameterized Systems by Dynamic Induction on Diagrams. - Zohar Manna; Henny Sipma (CAV, 1999)

Visual Verification of Temporal Properties. - Zohar Manna (TIME, 1999)

Deductive Model Checking. - Henny Sipma; Tomás E. Uribe; Zohar Manna (Formal Methods Syst. Des., 1999)

Alternating the Temporal Picture for Safety. - Zohar Manna; Henny Sipma (ICALP, 2000)

Verification of Clocked and Hybrid Systems. - Yonit Kesten; Zohar Manna; Amir Pnueli (Acta Informatica, 2000)

The 'Cash-Point' Service: A Verification Case Study Using STeP. - Anca Browne; Bernd Finkbeiner; Zohar Manna; Henny Sipma (Formal Aspects Comput., 2000)

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. - Nikolaj S. Bjørner; Anca Browne; Michael Colón; Bernd Finkbeiner; Zohar Manna; Henny Sipma; Tomás E. Uribe (Formal Methods Syst. Des., 2000)

Deductive verification of real-time systems using STeP. - Nikolaj S. Bjørner; Zohar Manna; Henny Sipma; Tomás E. Uribe (Theor. Comput. Sci., 2001)

Combining Decision Procedures. - Zohar Manna; Calogero G. Zarba (10th Anniversary Colloquium of UNU/IIST, 2002)

Petri Net Analysis Using Invariant Generation. - Sriram Sankaranarayanan 001; Henny Sipma; Zohar Manna (Verification: Theory and Practice, 2003)

Event Correlation: Language and Semantics. - César Sánchez 001; Sriram Sankaranarayanan 001; Henny Sipma; Ting Zhang 001; David L. Dill; Zohar Manna (EMSOFT, 2003)

Decision Procedures for Recursive Data Structures with Integer Constraints. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (IJCAR, 2004)

Non-linear loop invariant generation using Gröbner bases. - Sriram Sankaranarayanan 001; Henny Sipma; Zohar Manna (POPL, 2004)

Constraint-Based Linear-Relations Analysis. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (SAS, 2004)

Term Algebras with Length Function and Bounded Quantifier Alternation. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (TPHOLs, 2004)

Termination and Invariance Analysis of Loops. - Aaron R. Bradley; Zohar Manna (ATVA, 2005)

The Decidability of the First-Order Theory of Knuth-Bendix Order. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (CADE, 2005)

Final Semantics for Event-Pattern Reactive Programs. - César Sánchez 001; Henny B. Sipma; Matteo Slanina; Zohar Manna (CALCO, 2005)

Linear Ranking with Reachability. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (CAV, 2005)

Termination Analysis of Integer Linear Loops. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (CONCUR, 2005)

Thread Allocation Protocols for Distributed Real-Time and Embedded Systems. - César Sánchez 001; Henny B. Sipma; Venkita Subramonian; Christopher D. Gill; Zohar Manna (FORTE, 2005)

Expressive Completeness of an Event-Pattern Reactive Programming Language. - César Sánchez 001; Matteo Slanina; Henny B. Sipma; Zohar Manna (FORTE, 2005)

Decision Procedures for Queues with Integer Constraints. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (FSTTCS, 2005)

The Polyranking Principle. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (ICALP, 2005)

LOLA: Runtime Monitoring of Synchronous Systems. - Ben D'Angelo; Sriram Sankaranarayanan 001; César Sánchez 001; Will Robinson; Bernd Finkbeiner; Henny B. Sipma; Sandeep Mehrotra; Zohar Manna (TIME, 2005)

Termination of Polynomial Programs. - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (VMCAI, 2005)

Scalable Analysis of Linear Systems Using Mathematical Programming. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (VMCAI, 2005)

Efficient distributed deadlock avoidance with liveness guarantees. - César Sánchez 001; Henny B. Sipma; Zohar Manna; Christopher D. Gill (EMSOFT, 2006)

Fixed Point Iteration for Computing the Time Elapse Operator. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (HSCC, 2006)

Verification Constraint Problems with Strengthening. - Aaron R. Bradley; Zohar Manna (ICTAC, 2006)

Proving ATL* Properties of Infinite-State Systems. - Matteo Slanina; Henny B. Sipma; Zohar Manna (ICTAC, 2006)

On efficient distributed deadlock avoidance for real-time and embedded systems. - César Sánchez 001; Henny B. Sipma; Zohar Manna; Venkita Subramonian; Christopher D. Gill (IPDPS, 2006)

Distributed Priority Inheritance for Real-Time and Embedded Systems. - César Sánchez 001; Henny B. Sipma; Christopher D. Gill; Zohar Manna (OPODIS, 2006)

What's Decidable About Arrays? - Aaron R. Bradley; Zohar Manna; Henny B. Sipma (VMCAI, 2006)

Efficient Strongly Relational Polyhedral Analysis. - Sriram Sankaranarayanan 001; Michael Colón; Henny B. Sipma; Zohar Manna (VMCAI, 2006)

Decision procedures for term algebras with integer constraints. - Ting Zhang 001; Henny B. Sipma; Zohar Manna (Inf. Comput., 2006)

The calculus of computation - decision procedures with applications to verification. - Aaron R. Bradley; Zohar Manna (Springer, 2007)

A Family of Distributed Deadlock Avoidance Protocols and Their Reachable State Spaces. - César Sánchez 001; Henny B. Sipma; Zohar Manna (FASE, 2007)

Checking Safety by Inductive Generalization of Counterexamples to Induction. - Aaron R. Bradley; Zohar Manna (FMCAD, 2007)

Generating Efficient Distributed Deadlock Avoidance Controllers. - César Sánchez 001; Henny B. Sipma; Zohar Manna (IPDPS, 2007)

Verifying Balanced Trees. - Zohar Manna; Henny B. Sipma; Ting Zhang 001 (LFCS, 2007)

The Reaction Algebra: A Formal Language for Event Correlation. - César Sánchez 001; Matteo Slanina; Henny B. Sipma; Zohar Manna (Pillars of Computer Science, 2008)

Property-directed incremental invariant generation. - Aaron R. Bradley; Zohar Manna (Formal Aspects Comput., 2008)

Deductive verification of alternating systems. - Matteo Slanina; Henny B. Sipma; Zohar Manna (Formal Aspects Comput., 2008)

Constructing invariants for hybrid systems. - Sriram Sankaranarayanan 001; Henny B. Sipma; Zohar Manna (Formal Methods Syst. Des., 2008)

Temporal Verification of Reactive Systems: Response. - Zohar Manna; Amir Pnueli (Essays in Memory of Amir Pnueli, 2010)