Zohar Manna
According to our database1, Zohar Manna
Awards
ACM Fellow
ACM Fellow 1994, "".
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:
-
at viaf.org
-
at isni.org
-
at id.loc.gov
-
at d-nb.info
-
at dl.acm.org
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 in System Design, 2008
Deductive verification of alternating systems.
Formal Asp. Comput., 2008
Property-directed incremental invariant generation.
Formal Asp. 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
Constructing Invariants for Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 7th International Workshop, 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 in System Design, 2000
The 'Cash-Point' Service: A Verification Case Study Using STeP.
Formal Asp. Comput., 2000
Verification of Clocked and Hybrid Systems.
Acta Inf., 2000
Alternating the Temporal Picture for Safety.
Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000
1999
Deductive Model Checking.
Formal Methods in System Design, 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
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
Deductive Verification of Real-Time Systems Using STeP.
Proceedings of the Transformation-Based Reactive Systems Development, 1997
Verification of Progress Properties.
Proceedings of the 1997 Joint Conf. on Declarative Programming, 1997
1996
Verification of Clocked and Hybrid Systems.
Proceedings of the Lectures on Embedded Systems, European Educational Forum, 1996
Deductive Model Checking.
Proceedings of the Computer Aided Verification, 8th International Conference, 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.
WOCFAI, 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 Inf., 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
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
A Temporal Proof Methodology for Reactive Systems.
Proceedings of the Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28, 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-3-540-97664-6, 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
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
Completing the Temporal Picture.
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 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. Reasoning, 1987
Specification and Verification of Concurrent Programs by forall-Automata.
Proceedings of the Temporal Logic in Specification, 1987
Temporal Logic Programming.
Proceedings of the 1987 Symposium on Logic Programming, San Francisco, California, USA, August 31, 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 Software, 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.
Logic Programming: Functions, Relations, and Equations, 1986
1985
Nonclausal Temporal Deduction.
Proceedings of the Logics of Programs, 1985
The Origin of the Binary-Search Paradigm.
Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, 1985
Special Relations in Automated Deduction.
Proceedings of the Automata, 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.
LISP and Functional Programming, 1984
1983
The Temporal Logic of Branching Time.
Acta Inf., 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 Inf., 1981
The Temporal Logic of Branching Time.
Proceedings of the Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, 1981
Synthesis of Communicating Processes from Temporal Logic Specifications.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, 1981
Verification of Concurrent Programs: Temporal Proof Principles.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, 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.
IFIP Congress, 1980
1979
Synthesis: Dreams - Programs.
IEEE Trans. Software Eng., 1979
Proving Termination with Multiset Orderings.
Commun. ACM, 1979
A Deductive Approach to Program Synthesis.
Proceedings of the Sixth International Joint Conference on Artificial Intelligence, 1979
The Modal Logic of Programs.
Proceedings of the Automata, 1979
Proving termination with Multiset Orderings.
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
Inference Rules for Program Annotation.
Proceedings of the 3rd International Conference on Software Engineering, 1978
1977
The Evolution of Programs: Automatic Program Modification.
IEEE Trans. Software Eng., 1977
The automatic synthesis of recursive programs.
SIGART Newsletter, 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
Is 'Sometime' Sometimes Better Than 'Always'? Intermittent Assertions in Proving Program Correctness.
Proceedings of the 2nd International Conference on Software Engineering, 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 Inf., 1975
The Optimal Fixedpoint of Recursive Programs
Proceedings of the 7th Annual ACM Symposium on Theory of Computing, 1975
Knowledge and Reasoning in Program Synthesis.
Proceedings of the Advance Papers of the Fourth International Joint Conference on Artificial Intelligence, 1975
1974
Axiomatic Approach to Total Correctness of Programs.
Acta Inf., 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
Fixpoint Approach to the Theory of Computation.
ICALP, 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.
IFIP Congress (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