BibSLEIGH — Amir

Travelled to:

1 × Belgium
1 × Canada
1 × Poland
1 × Singapore
1 × The Netherlands
2 × Austria
2 × Denmark
2 × Finland
2 × Greece
2 × Israel
28 × USA
3 × Portugal
4 × Spain
4 × United Kingdom
5 × Germany
5 × Italy
6 × France

Collaborated with:

Z.Manna L.D.Zuck Y.Kesten ∅ N.Piterman O.Maler I.Balaban R.Rosner D.Harel M.Siegel T.Arons E.Shahar Y.Sa'ar D.Peled O.Strichman A.Zaks H.Kugler Y.Fang J.Stavi O.Lichtenstein R.Sherman A.Cohen E.Y.Chang T.A.Henzinger H.Barringer R.Kuiper D.J.Lehmann M.Ben-Ari S.Ruah A.Zaks O.Kupferman R.Zarhi G.Slutzki C.W.Barrett B.Goldberg Y.Hu U.Klein C.Plock P.Niebert D.Nickovic R.Bloem S.J.Galler B.Jobstmann M.Weiglhofer A.Podelski A.Rybalchenko J.Xu L.Raviv E.Singerman S.Katz E.Harel D.Ron F.Rosemberg D.Shasha W.Ewald S.Cohen S.Hart M.Sharir J.Y.Halpern M.J.Stern E.J.A.Hubbard M.Talupur N.Sinha Y.Rodeh A.Klein G.Raanan M.Bozga S.Yovine H.McGuire A.Kleinman Y.Moscowitz E.Y.Shapiro J.P.Schmidt D.M.Gabbay S.Shelah Y.Lu Y.Bontemps J.Hooman M.v.d.Zwaag J.Xu M.Marcus H.Lachover A.Naamad M.Politi A.Shtull-Trauring

Talks about:

verif (20) logic (16) tempor (15) system (13) model (11) abstract (9) program (9) specif (8) analysi (7) deduct (7)

Person: Amir Pnueli

DBLP: Pnueli:Amir

Contributed to:

2012

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1991

1990

1989

1988

1987

1986

1985

1984

1983

1982

1981

1980

1979

1977

1969

Wrote 93 papers:

VMCAI-2012-KleinPP #effectiveness #specification #synthesis: Effective Synthesis of Asynchronous Systems from GR(1) Specifications (UK, NP, AP), pp. 283–298.
CAV-2010-PnueliSZ #algorithm #framework #named #verification: Jtlv: A Framework for Developing Verification Algorithms (AP, YS, LDZ), pp. 171–174.
FASE-2009-KuglerPP #requirements #synthesis: Controller Synthesis from LSC Requirements (HK, CP, AP), pp. 79–93.
CAV-2008-CohenPZ #memory management #transaction #verification: Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses (AC, AP, LDZ), pp. 121–134.
CAV-2008-NiebertPP #model checking: Discriminative Model Checking (PN, DP, AP), pp. 504–516.
FM-2008-ZaksP #compilation #named #program analysis #validation: CoVaC: Compiler Validation by Program Analysis of the Cross-Product (AZ, AP), pp. 35–51.
PASTE-2008-ZaksP #compilation #program analysis #validation: Program analysis for compiler validation (AZ, AP), pp. 1–7.
VMCAI-2008-PnueliS: All You Need Is Compassion (AP, YS), pp. 233–247.
CAV-2007-MalerNP #bound #on the: On Synthesizing Controllers from Bounded-Response Properties (OM, DN, AP), pp. 95–107.
COCV-2007-BloemGJPPW #hardware: Specify, Compile, Run: Hardware from PSL (RB, SJG, BJ, NP, AP, MW), pp. 3–16.
DATE-2007-BloemGJPPW #automation #case study #hardware #interactive #specification #synthesis: Interactive presentation: Automatic hardware synthesis from specifications: a case study (RB, SJG, BJ, NP, AP, MW), pp. 1188–1193.
TACAS-2007-KuglerPSH #framework #logic #modelling #predict: “Don’t Care” Modeling: A Logical Framework for Developing Predictive System Models (HK, AP, MJS, EJAH), pp. 343–357.
VMCAI-2007-BalabanPZ #analysis: Shape Analysis of Single-Parent Heaps (IB, AP, LDZ), pp. 91–105.
FM-2006-PnueliZ #model checking #runtime #verification: PSL Model Checking and Run-Time Verification Via Testers (AP, AZ), pp. 573–586.
ICALP-v2-2006-BalabanPZ #distributed #protocol #safety: Invisible Safety of Distributed Protocols (IB, AP, LDZ), pp. 528–539.
LICS-2006-PitermanP #game studies #performance: Faster Solutions of Rabin and Streett Games (NP, AP), pp. 275–284.
VMCAI-2006-BalabanCP #abstraction #ranking #recursion #source code: Ranking Abstraction of Recursive Programs (IB, AC, AP), pp. 267–281.
VMCAI-2006-PitermanPS #design #synthesis: Synthesis of Reactive(1) Designs (NP, AP, YS), pp. 364–380.
CAV-2005-BalabanFPZ #invariant #named #verification: IIV: An Invisible Invariant Verifier (IB, YF, AP, LDZ), pp. 408–412.
CAV-2005-BarrettFGHPZ #compilation #named #optimisation #validation: TVOC: A Translation Validator for Optimizing Compilers (CWB, YF, BG, YH, AP, LDZ), pp. 291–295.
COCV-J-2005-HuBGP #optimisation #validation: Validating More Loop Optimizations (YH, CWB, BG, AP), pp. 69–84.
TACAS-2005-KuglerHPLB #logic #specification: Temporal Logic for Scenario-Based Specifications (HK, DH, AP, YL, YB), pp. 445–460.
TACAS-2005-PnueliPR #analysis: Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems (AP, AP, AR), pp. 124–139.
VMCAI-2005-BalabanPZ #abstraction #analysis: Shape Analysis by Predicate Abstraction (IB, AP, LDZ), pp. 164–180.
VMCAI-2005-Pnueli #abstraction #liveness: Abstraction for Liveness (AP), p. 146.
CAV-2004-TalupurSSP #logic: Range Allocation for Separation Logic (MT, NS, OS, AP), pp. 148–161.
FoSSaCS-2004-MalerP #on the: On Recognizable Timed Languages (OM, AP), pp. 348–362.
TACAS-2004-FangPPZ #liveness #ranking: Liveness with Incomprehensible Ranking (YF, NP, AP, LDZ), pp. 482–496.
UML-2004-AronsHKPZ #deduction #modelling #uml #verification: Deductive Verification of UML Models in TLPVS (TA, JH, HK, AP, MvdZ), pp. 335–349.
VMCAI-2004-FangPPZ #liveness #ranking: Liveness with Invisible Ranking (YF, NP, AP, LDZ), pp. 223–238.
CAV-2003-KestenPP #simulation: Bridging the Gap between Fair Simulation and Trace Inclusion (YK, NP, AP), pp. 381–393.
FoSSaCS-2003-AronsPZ #abstraction #probability #verification: Parameterized Verification by Probabilistic Abstraction (TA, AP, LDZ), pp. 87–102.
VMCAI-2003-PnueliZ #abstraction #model checking: Model-Checking and Abstraction to the Aid of Parameterized Systems (AP, LDZ), p. 4.
CAV-2002-PnueliXZ #abstraction #liveness: Liveness with (0, 1, infty)-Counter Abstraction (AP, JX, LDZ), pp. 107–122.
VMCAI-2002-ZuckPK #automation #probability #verification: Automatic Verification of Probabilistic Free Choice (LDZ, AP, YK), pp. 208–224.
CAV-2001-AronsPRXZ #automation #induction #verification: Parameterized Verification with Automatically Computed Inductive Assertions (TA, AP, SR, JX, LDZ), pp. 221–234.
TACAS-2001-PnueliRZ #automation #deduction #invariant #verification: Automatic Deductive Verification with Invisible Invariants (AP, SR, LDZ), pp. 82–97.
CAV-2000-Pnueli #abstraction #composition #deduction #explosion #symmetry: Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion (AP), p. 1.
CAV-2000-PnueliS #liveness #verification: Liveness and Acceleration in Parameterized Verification (AP, ES), pp. 328–343.
TACAS-2000-AronsP #comparison #execution #verification: A Comparison of Two Verification Methods for Speculative Instruction Execution (TA, AP), pp. 487–502.
CAV-1999-PnueliRSS #similarity: Deciding Equality Formulas by Small Domains Instantiations (AP, YR, OS, MS), pp. 455–469.
CSL-1999-KestenP #abstraction #liveness #verification: Verifying Liveness by Augmented Abstraction (YK, AP), pp. 141–156.
FM-v1-1999-KestenKPR #analysis #deduction #model checking #verification: A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software (YK, AK, AP, GR), pp. 173–194.
CADE-1998-Pnueli #deduction #verification: Deductive vs. Model-Theoretic Approaches to Formal Verification (AP), p. 301.
FM-1998-PnueliSS #validation: Translation Validation: From DC+ to C* (AP, OS, MS), pp. 137–150.
ICALP-1998-KestenPR #algorithm #linear #logic #specification #verification: Algorithmic Verification of Linear Temporal Logic Specifications (YK, AP, LoR), pp. 1–16.
ICALP-1998-PnueliSS #validation: Translation Validation for Synchronous Languages (AP, OS, MS), pp. 235–246.
TACAS-1998-PnueliSS #validation: Translation Validation (AP, MS, ES), pp. 151–166.
CAV-1997-BozgaMPY #automaton #verification: Some Progress in the Symbolic Verification of Timed Automata (MB, OM, AP, SY), pp. 179–190.
CAV-1997-KestenMMPS #model checking: Symbolic Model Checking with Rich ssertional Languages (YK, OM, MM, AP, ES), pp. 424–435.
CAV-1996-PnueliS #algorithm #deduction #framework #platform #verification: A Platform for Combining Deductive with Algorithmic Verification (AP, ES), pp. 184–195.
LICS-1995-KestenP #proving: A Complete Proof Systems for QPTL (YK, AP), pp. 2–12.
LICS-1995-KupfermanP: Once and For All (OK, AP), pp. 25–35.
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.
CAV-1993-MalerP #analysis #multi #reachability: Reachability Analysis of Planar Multi-limear Systems (OM, AP), pp. 194–209.
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.
LICS-1991-PeledKP #logic #proving #specification: Specifying and Proving Serializability in Temporal Logic (DP, SK, AP), pp. 232–244.
POPL-1991-HenzingerMP #proving #realtime: Temporal Proof Methodologies for Real-time Systems (TAH, ZM, AP), pp. 353–366.
POPL-1991-KleinmanMPS #communication #logic: Communication with Directed Logic Variables (AK, YM, AP, EYS), pp. 221–232.
ICALP-1990-PeledP #liveness #partial order #proving: Proving Partial Order Liveness Properties (DP, AP), pp. 553–571.
LICS-1990-HarelLP #logic: Explicit Clock Temporal Logic (EH, OL, AP), pp. 402–413.
ICALP-1989-MannaP: Completing the Temporal Picture (ZM, AP), pp. 534–558.
ICALP-1989-PnueliR #on the #synthesis: On the Synthesis of an Asynchronous Reactive Module (AP, RR), pp. 652–671.
POPL-1989-PnueliR #on the #synthesis: On the Synthesis of a Reactive Module (AP, RR), pp. 179–190.
ICSE-1988-HarelLNPPSS #development: STATEMATE; A Working Environment for the Development of Complex Reactive Systems (DH, HL, AN, AP, MP, RS, AST), pp. 396–406.
LICS-1987-HarelPSS #on the #semantics: On the Formal Semantics of Statecharts (DH, AP, JPS, RS), pp. 54–64.
POPL-1987-MannaP #concurrent #source code #specification #verification: Specification and Verification of Concurrent Programs By Forall-Automata (ZM, AP), pp. 1–12.
LICS-1986-PnueliZ #probability #verification: Probabilistic Verification by Tableaux (AP, LDZ), pp. 322–331.
LICS-1986-RosnerP #logic: A Choppy Logic (RR, AP), pp. 306–313.
POPL-1986-BarringerKP #concurrent #logic: A Really Abstract Concurrent Model and its Temporal Logic (HB, RK, AP), pp. 173–183.
ICALP-1985-Pnueli #branch #linear #logic #semantics: Linear and Branching Structures in the Semantics and Logics of Reactive Systems (AP), pp. 15–32.
POPL-1985-LichtensteinP #concurrent #finite #linear #source code #specification: Checking That Finite State Concurrent Programs Satisfy Their Linear Specification (OL, AP), pp. 97–107.
ICALP-1984-RonRP #csp #hardware #implementation #verification: A Hardware Implementation of the CSP Primitives and its Verification (DR, FR, AP), pp. 423–435.
POPL-1984-ShashaPE #network #protocol #verification: Temporal Verification of Carrier-Sense Local Area Network Protocols (DS, AP, WE), pp. 54–65.
STOC-1984-BarringerKP #logic #specification: Now You May Compose Temporal Logic Specifications (HB, RK, AP), pp. 51–63.
ICALP-1983-CohenLP #distributed #problem #symmetry: Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (SC, DJL, AP), pp. 128–136.
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.
STOC-1983-Pnueli #algorithm #on the #probability: On the Extremely Fair Treatment of Probabilistic Algorithms (AP), pp. 278–290.
POPL-1982-HartSP #concurrent #probability #source code #termination: Termination of Probabilistic Concurrent Programs (SH, MS, AP), pp. 1–6.
POPL-1982-ShermanPH #logic #process: Is the Interesting Part of Process Logic Uninteresting — A Translation from PL to PDL (RS, AP, DH), pp. 347–360.
ICALP-1981-Ben-AriHP #finite #logic #modelling: Finite Models for Deterministic Propositional Dynamic Logic (MBA, JYH, AP), pp. 249–263.
ICALP-1981-LehmannPS #concurrent #termination: Impartiality, Justice and Fairness: The Ethics of Concurrent Termination (DJL, AP, JS), pp. 264–277.
ICALP-1981-PnueliZ #equation #specification: Realizing an Equational Specification (AP, RZ), pp. 459–478.
POPL-1981-Ben-AriMP #branch #logic: The Temporal Logic of Branching Time (MBA, ZM, AP), pp. 164–176.
POPL-1980-GabbayPSS #on the: On the Temporal Basis of Fairness (DMG, AP, SS, JS), pp. 163–173.
POPL-1980-MannaP #problem: Synchronous Schemes and Their Decision Problems (ZM, AP), pp. 62–67.
ICALP-1979-MannaP #logic #source code: The Modal Logic of Programs (ZM, AP), pp. 385–409.
ICALP-1977-PnueliS #problem #source code: Simple Programs and Their Decision Problems (AP, GS), pp. 380–390.
STOC-1977-HarelPS #axiom #deduction #proving #recursion #source code: A Complete Axiomatic System for Proving Deductions about Recursive Programs (DH, AP, JS), pp. 249–260.
STOC-1969-MannaP #formal method #recursion: Formalization of Properties of Recursively Defined Functions (ZM, AP), pp. 201–210.