Zohar Manna

Affiliations:
  • Stanford University, USA


According to our database1, Zohar Manna authored at least 171 papers between 1969 and 2010.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 1994, "".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2010
Temporal Verification of Reactive Systems: Response.
Proceedings of the Time for Verification, 2010

2008
Constructing invariants for hybrid systems.
Formal Methods Syst. Des., 2008

Deductive verification of alternating systems.
Formal Aspects Comput., 2008

Property-directed incremental invariant generation.
Formal Aspects Comput., 2008

The Reaction Algebra: A Formal Language for Event Correlation.
Proceedings of the Pillars of Computer Science, 2008

2007
Verifying Balanced Trees.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

Generating Efficient Distributed Deadlock Avoidance Controllers.
Proceedings of the 21th International Parallel and Distributed Processing Symposium (IPDPS 2007), 2007

Checking Safety by Inductive Generalization of Counterexamples to Induction.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

A Family of Distributed Deadlock Avoidance Protocols and Their Reachable State Spaces.
Proceedings of the Fundamental Approaches to Software Engineering, 2007

The calculus of computation - decision procedures with applications to verification.
Springer, 2007

2006
Decision procedures for term algebras with integer constraints.
Inf. Comput., 2006

Efficient Strongly Relational Polyhedral Analysis.
Proceedings of the Verification, 2006

What's Decidable About Arrays?
Proceedings of the Verification, 2006

Distributed Priority Inheritance for Real-Time and Embedded Systems.
Proceedings of the Principles of Distributed Systems, 10th International Conference, 2006

On efficient distributed deadlock avoidance for real-time and embedded systems.
Proceedings of the 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), 2006

Proving ATL* Properties of Infinite-State Systems.
Proceedings of the Theoretical Aspects of Computing, 2006

Verification Constraint Problems with Strengthening.
Proceedings of the Theoretical Aspects of Computing, 2006

Fixed Point Iteration for Computing the Time Elapse Operator.
Proceedings of the Hybrid Systems: Computation and Control, 9th International Workshop, 2006

Efficient distributed deadlock avoidance with liveness guarantees.
Proceedings of the 6th ACM & IEEE International conference on Embedded software, 2006

2005
Scalable Analysis of Linear Systems Using Mathematical Programming.
Proceedings of the Verification, 2005

Termination of Polynomial Programs.
Proceedings of the Verification, 2005

LOLA: Runtime Monitoring of Synchronous Systems.
Proceedings of the 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 2005

The Polyranking Principle.
Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

Decision Procedures for Queues with Integer Constraints.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

Expressive Completeness of an Event-Pattern Reactive Programming Language.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

Thread Allocation Protocols for Distributed Real-Time and Embedded Systems.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005

Termination Analysis of Integer Linear Loops.
Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

Linear Ranking with Reachability.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Final Semantics for Event-Pattern Reactive Programs.
Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

The Decidability of the First-Order Theory of Knuth-Bendix Order.
Proceedings of the Automated Deduction, 2005

Termination and Invariance Analysis of Loops.
Proceedings of the Automated Technology for Verification and Analysis, 2005

2004
Term Algebras with Length Function and Bounded Quantifier Alternation.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Constraint-Based Linear-Relations Analysis.
Proceedings of the Static Analysis, 11th International Symposium, 2004

Non-linear loop invariant generation using Gröbner bases.
Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

Decision Procedures for Recursive Data Structures with Integer Constraints.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Event Correlation: Language and Semantics.
Proceedings of the Embedded Software, Third International Conference, 2003

Petri Net Analysis Using Invariant Generation.
Proceedings of the Verification: Theory and Practice, 2003

2002
Combining Decision Procedures.
Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

2001
Deductive verification of real-time systems using STeP.
Theor. Comput. Sci., 2001

2000
Verifying Temporal Properties of Reactive Systems: A STeP Tutorial.
Formal Methods Syst. Des., 2000

The 'Cash-Point' Service: A Verification Case Study Using STeP.
Formal Aspects Comput., 2000

Verification of Clocked and Hybrid Systems.
Acta Informatica, 2000

Alternating the Temporal Picture for Safety.
Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000

1999
Deductive Model Checking.
Formal Methods Syst. Des., 1999

Visual Verification of Temporal Properties.
Proceedings of the 6th International Workshop on Temporal Representation and Reasoning, 1999

Verification of Parameterized Systems by Dynamic Induction on Diagrams.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems.
Proceedings of the International Workshop Tool Support for System Specification, 1998

Deductive Verification of Hybrid Systems Using STeP.
Proceedings of the Hybrid Systems: Computation and Control, First International Workshop, 1998

Visual Abstractions for Temporal Verification.
Proceedings of the Algebraic Methodology and Software Technology, 1998

1997
Automatic Generation of Invariants and Intermediate Assertions.
Theor. Comput. Sci., 1997

Visual Verification of Reactive Systems.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1997

Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification.
Proceedings of the STACS 97, 14th Annual Symposium on Theoretical Aspects of Computer Science, Lübeck, Germany, February 27, 1997

Abstraction and Modular Verification of Infinite-State Reactive Systems.
Proceedings of the Requirements Targeting Software and Systems Engineering, 1997

Deductive Verification of Modular Systems.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

Verification of Progress Properties.
Proceedings of the 1997 Joint Conf. on Declarative Programming, 1997

1996
STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Temporal Verification by Diagram Transformations.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Hierarchical Verification Using Verification Diagrams.
Proceedings of the Concurrency and Parallelism, 1996

1995
A Temporal Plan Theory.
Proceedings of the Second World Conference on the Fundamentals of Artificial Intelligence, 1995

STeP: The Stanford Temporal Prover.
Proceedings of the TAPSOFT'95: Theory and Practice of Software Development, 1995

Verifying Clocked Transition Systems.
Proceedings of the Hybrid Systems III: Verification and Control, 1995

Generalized Temporal Verification Diagrams.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1995

Automatic Generation of Invariants and Assertions.
Proceedings of the Principles and Practice of Constraint Programming, 1995

Verification in Continuous Time by Discrete Reasoning.
Proceedings of the Algebraic Methodology and Software Technology, 1995

Differential BDDs.
Proceedings of the Computer Science Today: Recent Trends and Developments, 1995

Temporal verification of reactive systems - safety.
Springer, ISBN: 978-0-387-94459-3, 1995

1994
Temporal Proof Methodologies for Timed Transition Systems
Inf. Comput., August, 1994

Temporal Verification Diagrams.
Proceedings of the Theoretical Aspects of Computer Software, 1994

Compositional Verification of Real-Time Systems
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Annotation-Based Deduction in Temporal Logic.
Proceedings of the Temporal Logic, First International Conference, 1994

Specification and Verification of Controlled Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

Prooving Safety Properties of Hybrid Systems.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

Beyond Model Checking.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

Realizability and Synthesis of Reactive Modules.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993
Models for Reactivity.
Acta Informatica, 1993

Temporal Verification of Simulation and Refinement.
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993

A Decision Algorithm for Full Propositional Temporal Logic.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

Verification of parameterized programs.
Proceedings of the Specification and validation methods, 1993

The deductive foundations of computer programming - a one-volume version of "The logical basis for computer programming".
Addison-Wesley, ISBN: 978-0-201-54886-0, 1993

1992
Fundamentals of Deductive Program Synthesis.
IEEE Trans. Software Eng., 1992

Time for Concurrency.
Proceedings of the Future Tendencies in Computer Science, 1992

What Good Are Digital Clocks?
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Characterization of Temporal Property Classes.
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

Verifying Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

Towards Refining Temporal Specifications into Hybrid Systems.
Proceedings of the Hybrid Systems, 1992

The Special-Relation Rules are Incomplete.
Proceedings of the Automated Deduction, 1992

The temporal logic of reactive and concurrent systems - specification.
Springer, ISBN: 978-1-4612-0931-7, 1992

1991
Completing the Temporal Picture.
Theor. Comput. Sci., 1991

From Timed to Hybrid Systems.
Proceedings of the Real-Time: Theory in Practice, 1991

Timed Transition Systems.
Proceedings of the Real-Time: Theory in Practice, 1991

Temporal Proof Methodologies for Real-time Systems.
Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991

On the Faithfulness of Formal Models.
Proceedings of the Mathematical Foundations of Computer Science 1991, 1991

Monotonicity Properties in Automated Deduction.
Proceedings of the Artificial and Mathematical Theory of Computation, 1991

1990
Nonclausal Deduction in First-Order Temporal Logic
J. ACM, April, 1990

A Hierarchy of Temporal Properties.
Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, 1990

A temporal proof methodology for reactive systems.
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

An interleaving model for real-time.
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990

1989
Temporal Logic Programming.
J. Symb. Comput., 1989

1988
The anchored version of the temporal framework.
Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988

1987
The Origin of a Binary-Search Paradigm.
Sci. Comput. Program., 1987

How to Clear a Block: A Theory of Plans.
J. Autom. Reason., 1987

Specification and Verification of Concurrent Programs By Forall-Automata.
Proceedings of the Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, 1987

A Hierarchy of Temporal Properties (Abstract).
Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987

The Deductive Synthesis of Imperative LISP Programs.
Proceedings of the 6th National Conference on Artificial Intelligence. Seattle, 1987

1986
Tablog: Functional and Relational Programming in One Framework.
IEEE Softw., 1986

Special relations in automated deduction.
J. ACM, 1986

Towards Deductive Synthesis of Dataflow Networks
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

A Timely Resolution
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

How to Clear a Block: Plan Formation in Situational Logic.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

Modal Theorem Proving.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

TABLOG: A New Approach To Logic Programming.
Proceedings of the Logic Programming: Functions, Relations, and Equations, 1986

1985
Nonclausal Temporal Deduction.
Proceedings of the Logics of Programs, 1985

Deduction with Relation Matching.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1985

1984
Synthesis of Communicating Processes from Temporal Logic Specifications.
ACM Trans. Program. Lang. Syst., 1984

Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.
Sci. Comput. Program., 1984

TABLOG: The Deductive-Tableau Programming Language.
Proceedings of the 1984 ACM Conference on LISP and Functional Programming, 1984

1983
The Temporal Logic of Branching Time.
Acta Informatica, 1983

How to Cook a Temporal Proof System for Your Pet Language.
Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983

Reasoning in Interval Temporal Logic.
Proceedings of the Logics of Programs, 1983

Proving Precedence Properties: The Temporal Way.
Proceedings of the Automata, 1983

A Hardware Semantics Based on Temporal Intervals.
Proceedings of the Automata, 1983

1981
Inference Rules for Program Annotation.
IEEE Trans. Software Eng., 1981

Deductive Synthesis of the Unification Algorithm.
Sci. Comput. Program., 1981

Problematic Features of Programming Languages: A Situational-Calculus Approach.
Acta Informatica, 1981

Verification of Concurrent Programs: Temporal Proof Principles.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

1980
A Deductive Approach to Program Synthesis.
ACM Trans. Program. Lang. Syst., 1980

Synchronous Schemes and Their Decision Problems.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980

Logics of Programs.
Proceedings of the Information Processing, Proceedings of the 8th IFIP Congress 1980, Tokyo, Japan - October 6-9, 1980 and Melbourne, Australia, 1980

1979
Synthesis: Dreams - Programs.
IEEE Trans. Software Eng., 1979

Proving Termination with Multiset Orderings.
Commun. ACM, 1979

The Modal Logic of Programs.
Proceedings of the Automata, 1979

1978
The Logic of Computer Programming.
IEEE Trans. Software Eng., 1978

The Convergence of Functions to Fixedpoints of Recursive Definitions.
Theor. Comput. Sci., 1978

Is "Sometime" Sometimes Better Than "Always"? (Intermittent Assertions in Proving Program Correctness).
Commun. ACM, 1978

The Synthesis of Structure Changing Programs.
Proceedings of the 3rd International Conference on Software Engineering, 1978

DEDALUS - The DEDuctive ALgorithm Ur-Synthesizer.
Proceedings of the American Federation of Information Processing Societies: 1978 National Computer Conference, 1978

1977
The Evolution of Programs: Automatic Program Modification.
IEEE Trans. Software Eng., 1977

The automatic synthesis of recursive programs.
Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages, 1977

The Optimal Approach to Recursive Programs.
Commun. ACM, 1977

The Evolution of Programs: A System for Automatic Program Modification.
Proceedings of the Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, 1977

The Automatic Synthesis of Systems of Recursive Programs.
Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, 1977

1976
The Theoretical Aspects of the Optimal Fixed Point.
SIAM J. Comput., 1976

On the Power of Programming Features.
Comput. Lang., 1976

Logical Analysis of Programs.
Commun. ACM, 1976

1975
Translating Program Schemas to While-Schemas.
SIAM J. Comput., 1975

Knowledge and Reasoning in Program Synthesis.
Artif. Intell., 1975

A Closer Look at Termination.
Acta Informatica, 1975

The Optimal Fixedpoint of Recursive Programs
Proceedings of the 7th Annual ACM Symposium on Theory of Computing, 1975

Towards automatic debugging of programs.
Proceedings of the International Conference on Reliable Software 1975, 1975

1974
Axiomatic Approach to Total Correctness of Programs.
Acta Informatica, 1974

Knowledge and Reasoning in Program Synthesis.
Proceedings of the Programming Methodology, 4th Informatik Symposium, 1974

1973
Decidable Properties of Monadic Functional Schemas.
J. ACM, 1973

Inductive Methods for Proving Properties of Programs.
Commun. ACM, 1973

A Heuristic Approach to Program Verification.
Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, 1973

1972
Fix Point Approach to the Theory of Computation.
Commun. ACM, 1972

Program Schemas with Equality
Proceedings of the 4th Annual ACM Symposium on Theory of Computing, 1972

Recursive definitions of partial functions and their computations.
Proceedings of ACM Conference on Proving Assertions About Programs, 1972

Fixpoint Approach to the Theory of Computation.
Proceedings of the Automata, 1972

Computation of recursive programs: theory vs practice.
Proceedings of the American Federation of Information Processing Societies: AFIPS Conference Proceedings: 1972 Spring Joint Computer Conference, 1972

1971
Towards automatic program synthesis.
Proceedings of the Symposium on Semantics of Algorithmic Languages, 1971

Mathematical theory of partial correctness.
Proceedings of the Symposium on Semantics of Algorithmic Languages, 1971

Mathematical Theory of Partial Correctness.
J. Comput. Syst. Sci., 1971

Toward Automatic Program Synthesis.
Commun. ACM, 1971

The Translation of 'Go To' Programs to 'While' Programs.
Proceedings of the Information Processing, Proceedings of IFIP Congress 1971, Volume 1, 1971

1970
Formalization of Properties of Functional Programs.
J. ACM, 1970

The Correctness of Nondeterministic Programs.
Artif. Intell., 1970

Second-Order Mathematical Theory of Computation
Proceedings of the 2nd Annual ACM Symposium on Theory of Computing, 1970

Termination of programs represented as interpreted graphs.
Proceedings of the American Federation of Information Processing Societies: AFIPS Conference Proceedings: 1970 Spring Joint Computer Conference, 1970

1969
The Correctness of Programs.
J. Comput. Syst. Sci., 1969

Properties of Programs and the First-Order Predicate Calculus.
J. ACM, 1969

Formalization of Properties of Recursively Defined Functions
Proceedings of the 1st Annual ACM Symposium on Theory of Computing, 1969


  Loading...