BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Pnueli:Amir

Contributed to:

VMCAI 20122012
CAV 20102010
FASE 20092009
CAV 20082008
FM 20082008
PASTE 20082008
VMCAI 20082008
CAV 20072007
COCV 20072007
DATE 20072007
TACAS 20072007
VMCAI 20072007
FM 20062006
ICALP (2) 20062006
LICS 20062006
VMCAI 20062006
CAV 20052005
COCV 20052005
TACAS 20052005
VMCAI 20052005
CAV 20042004
FoSSaCS 20042004
TACAS 20042004
UML 20042004
VMCAI 20042004
CAV 20032003
FoSSaCS 20032003
VMCAI 20032003
CAV 20022002
VMCAI 20022002
CAV 20012001
TACAS 20012001
CAV 20002000
TACAS 20002000
CAV 19991999
CSL 19991999
World Congress on Formal Methods 19991999
CADE 19981998
FM-Trends 19981998
ICALP 19981998
TACAS 19981998
CAV 19971997
CAV 19961996
LICS 19951995
LICS 19941994
CAV 19931993
ICALP 19921992
LICS 19911991
POPL 19911991
ICALP 19901990
LICS 19901990
ICALP 19891989
POPL 19891989
ICSE 19881988
LICS 19871987
POPL 19871987
LICS 19861986
POPL 19861986
ICALP 19851985
POPL 19851985
ICALP 19841984
POPL 19841984
STOC 19841984
ICALP 19831983
POPL 19831983
STOC 19831983
POPL 19821982
ICALP 19811981
POPL 19811981
POPL 19801980
ICALP 19791979
ICALP 19771977
STOC 19771977
STOC 19691969

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.