BibSLEIGH — Zohar

Travelled to:

1 × Estonia
1 × Germany
1 × Ireland
1 × Spain
1 × Switzerland
1 × United Kingdom
18 × USA
2 × Austria
2 × France
2 × Greece
2 × Portugal
2 × The Netherlands
4 × Italy

Collaborated with:

A.Pnueli H.B.Sipma R.J.Waldinger H.Sipma M.Abadi N.Dershowitz A.R.Bradley S.Sankaranarayanan ∅ E.Y.Chang L.d.Alfaro T.E.Uribe T.Zhang T.A.Henzinger A.Anuchitanukul A.Shamir J.Vuillemin A.K.Chandra M.Colón C.Sánchez B.Jonsson Y.Malachi J.Y.Halpern B.C.Moszkowski M.Ben-Ari Y.Kesten H.McGuire N.Bjørner A.Browne A.Kapur H.Devarajan J.Lee

Talks about:

program (13) tempor (12) system (8) verif (6) deduct (5) logic (5) time (5) linear (4) relat (4) prove (4)

Person: Zohar Manna

DBLP: Manna:Zohar

Contributed to:

2007

2006

2005

2004

2000

1999

1997

1996

1994

1993

1992

1991

1989

1987

1986

1985

1984

1983

1981

1980

1979

1978

1977

1976

1975

1972

1970

1969

1995

Wrote 51 papers:

FASE-2007-SanchezSM #concurrent #distributed #product line #protocol: A Family of Distributed Deadlock Avoidance Protocols and Their Reachable State Spaces (CS, HBS, ZM), pp. 155–169.
VMCAI-2006-BradleyMS #array #decidability #question #what: What’s Decidable About Arrays? (ARB, ZM, HBS), pp. 427–442.
VMCAI-2006-SankaranarayananCSM #analysis #performance #relational: Efficient Strongly Relational Polyhedral Analysis (SS, MC, HBS, ZM), pp. 111–125.
CADE-2005-ZhangSM #decidability #first-order: The Decidability of the First-Order Theory of Knuth-Bendix Order (TZ, HBS, ZM), pp. 131–148.
CAV-2005-BradleyMS #linear #ranking #reachability: Linear Ranking with Reachability (ARB, ZM, HBS), pp. 491–504.
ICALP-2005-BradleyMS #principle #ranking: The Polyranking Principle (ARB, ZM, HBS), pp. 1349–1361.
VMCAI-2005-BradleyMS #polynomial #source code #termination: Termination of Polynomial Programs (ARB, ZM, HBS), pp. 113–129.
VMCAI-2005-SankaranarayananSM #analysis #linear #programming #scalability #using: Scalable Analysis of Linear Systems Using Mathematical Programming (SS, HBS, ZM), pp. 25–41.
IJCAR-2004-ZhangSM #constraints #data type #integer #recursion: Decision Procedures for Recursive Data Structures with Integer Constraints (TZ, HBS, ZM), pp. 152–167.
POPL-2004-SankaranarayananSM #generative #invariant #using: Non-linear loop invariant generation using Gröbner bases (SS, HS, ZM), pp. 318–329.
SAS-2004-SankaranarayananSM #analysis #constraints: Constraint-Based Linear-Relations Analysis (SS, HBS, ZM), pp. 53–68.
ICALP-2000-MannaS #safety: Alternating the Temporal Picture for Safety (ZM, HS), pp. 429–450.
CAV-1999-MannaS #diagrams #induction #verification: Verification of Parameterized Systems by Dynamic Induction on Diagrams (ZM, HS), pp. 25–41.
TACAS-1997-AlfaroM #verification #visual notation: Visual Verification of Reactive Systems (LdA, ZM, HBS, TEU), pp. 334–350.
CAV-1996-AlfaroM #diagrams #verification: Temporal Verification by Diagram Transformations (LdA, ZM), pp. 288–299.
CAV-1996-BjornerBCCKMSU #named #realtime #verification: STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems (NB, AB, EYC, MC, AK, ZM, HS, TEU), pp. 415–418.
CAV-1996-SipmaUM #deduction #model checking: Deductive Model Checking (HS, TEU, ZM), pp. 208–219.
CAV-1994-AnuchitanukulM #synthesis: Realizability and Synthesis of Reactive Modules (AA, ZM), pp. 156–168.
CAV-1994-Manna #model checking: Beyond Model Checking (ZM), pp. 220–221.
LICS-1994-ChangMP #composition #realtime #verification: Compositional Verification of Real-Time Systems (EYC, ZM, AP), pp. 458–465.
CAV-1993-KestenMMP #algorithm #logic: A Decision Algorithm for Full Propositional Temporal Logic (YK, ZM, HM, AP), pp. 97–109.
CADE-1992-MannaW: The Special-Relation Rules are Incomplete (ZM, RJW), pp. 492–506.
ICALP-1992-ChangMP: Characterization of Temporal Property Classes (EYC, ZM, AP), pp. 474–486.
ICALP-1992-HenzingerMP #question #what: What Good Are Digital Clocks? (TAH, ZM, AP), pp. 545–558.
POPL-1991-HenzingerMP #proving #realtime: Temporal Proof Methodologies for Real-time Systems (TAH, ZM, AP), pp. 353–366.
ICALP-1989-MannaP: Completing the Temporal Picture (ZM, AP), pp. 534–558.
POPL-1987-MannaP #concurrent #source code #specification #verification: Specification and Verification of Concurrent Programs By Forall-Automata (ZM, AP), pp. 1–12.
SLP-1987-AbadiM87 #logic programming: Temporal Logic Programming (MA, ZM), pp. 4–16.
CADE-1986-AbadiM #proving #theorem proving: Modal Theorem Proving (MA, ZM), pp. 172–189.
CADE-1986-MannaW #how #logic: How to Clear a Block: Plan Formation in Situational Logic (ZM, RJW), pp. 622–640.
LICS-1986-AbadiM: A Timely Resolution (MA, ZM), pp. 176–186.
LICS-1986-JonssonMW #data flow #deduction #network #synthesis #towards: Towards Deductive Synthesis of Dataflow Networks (BJ, ZM, RJW), pp. 26–37.
ICALP-1985-MannaW #automation #deduction: Special Relations in Automated Deduction (ZM, RJW), pp. 413–423.
LFP-1984-MalachiMW #named #programming language: TABLOG: The Deductive-Tableau Programming Language (YM, ZM, RJW), pp. 323–330.
ICALP-1983-HalpernMM #hardware #semantics: A Hardware Semantics Based on Temporal Intervals (JYH, ZM, BCM), pp. 278–291.
ICALP-1983-MannaP #precedence #proving: Proving Precedence Properties: The Temporal Way (ZM, AP), pp. 491–512.
POPL-1983-MannaP #how #proving: How to Cook a Temporal Proof System for Your Pet Language (ZM, AP), pp. 141–154.
POPL-1981-Ben-AriMP #branch #logic: The Temporal Logic of Branching Time (MBA, ZM, AP), pp. 164–176.
POPL-1980-MannaP #problem: Synchronous Schemes and Their Decision Problems (ZM, AP), pp. 62–67.
ICALP-1979-DershowitzM #multi #order #proving #termination: Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.
ICALP-1979-MannaP #logic #source code: The Modal Logic of Programs (ZM, AP), pp. 385–409.
ICSE-1978-DershowitzM: Inference Rules for Program Annotation (ND, ZM), pp. 158–167.
ICSE-1978-MannaW #source code #synthesis: The Synthesis of Structure Changing Programs (ZM, RJW), pp. 175–187.
POPL-1977-DershowitzM #automation #evolution #source code: The Evolution of Programs: A System for Automatic Program Modification (ND, ZM), pp. 144–154.
ICSE-1976-MannaW #correctness #proving: Is “Sometime” Sometimes Better Than “Always”? Intermittent Assertions in Proving Program Correctness (ZM, RJW), pp. 32–39.
STOC-1975-MannaS #recursion #source code: The Optimal Fixedpoint of Recursive Programs (ZM, AS), pp. 194–206.
ICALP-1972-MannaV #approach #fixpoint #formal method: Fixpoint Approach to the Theory of Computation (ZM, JV), pp. 273–291.
STOC-1972-ChandraM #similarity: Program Schemas with Equality (AKC, ZM), pp. 52–64.
STOC-1970-Manna #higher-order: Second-Order Mathematical Theory of Computation (ZM), pp. 158–168.
STOC-1969-MannaP #formal method #recursion: Formalization of Properties of Recursively Defined Functions (ZM, AP), pp. 201–210.
TAPSOFT-1995-MannaBBCCADKLSU #named #proving: STeP: The Stanford Temporal Prover (ZM, NB, AB, EYC, MC, LdA, HD, AK, JL, HS, TEU), pp. 793–794.