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 × Canada
1 × Germany
1 × Greece
1 × Italy
2 × France
2 × United Kingdom
3 × USA
Collaborated with:
∅ M.Abadi D.Doligez R.P.Kurshan F.B.Schneider S.Merz U.Engberg P.Grønning P.Wolper K.Chaudhuri D.Cousineau D.Ricketts H.Vanzetto H.Akhiani P.Harter J.Scheid M.R.Tuttle Y.Yu
Talks about:
verif (4) tla (4) system (3) proof (3) sometim (2) program (2) concurr (2) specif (2) constraint (1) unrealiz (1)

Person: Leslie Lamport

DBLP DBLP: Lamport:Leslie

Contributed to:

FM 20122012
IJCAR 20102010
World Congress on Formal Methods 19991999
TACAS 19961996
CAV 19931993
CAV 19921992
ICALP 19891989
LICS 19881988
POPL 19851985
POPL 19831983
POPL 19801980

Wrote 13 papers:

FM-2012-CousineauDLMRV #proving
TLA + Proofs (DC, DD, LL, SM, DR, HV), pp. 147–154.
IJCAR-2010-ChaudhuriDLM #proving #safety #verification
Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.
FM-v2-1999-AkhianiDHLSTY #verification
Cache Coherence Verification with TLA+ (HA, DD, PH, LL, JS, MRT, YY), pp. 1871–1872.
TACAS-1996-Lamport #proving
Managing Proofs (LL), p. 34.
CAV-1993-KurshanL #multi #verification
Verification of a Multiplier: 64 Bits and Beyond (RPK, LL), pp. 166–179.
CAV-1992-EngbergGL #concurrent #verification
Mechanical Verification of Concurrent Systems with TLA (UE, PG, LL), pp. 44–55.
CAV-1992-Lamport #verification
Computer-Hindered Verification (Humans Can Do It Too) (LL), p. 1.
ICALP-1989-AbadiLW #specification
Realizable and Unrealizable Specifications of Reactive Systems (MA, LL, PW), pp. 1–17.
LICS-1988-AbadiL #refinement
The Existence of Refinement Mappings (MA, LL), pp. 165–175.
POPL-1985-Lamport #concurrent #specification #what #why
What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority (LL), pp. 78–83.
POPL-1985-LamportS #alias #approach #constraints #named #type system
Constraints: A Uniform Approach to Aliasing and Typing (LL, FBS), pp. 205–216.
POPL-1983-Lamport #reasoning
Reasoning About Nonatomic Operations (LL), pp. 28–37.
POPL-1980-Lamport #logic #quote #source code
“Sometime” is Sometimes “Not Never” — On the Temporal Logic of Programs (LL), pp. 174–185.
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.