Leslie Lamport - MSR - INRIA

Leslie Lamport
Are you Leslie Lamport?

Claim your profile, edit publications, add additional information:

Contact Details

Leslie Lamport

Pubs By Year

Pub Categories

Computer Science - Logic in Computer Science (5)
Computer Science - Databases (1)
Computer Science - Software Engineering (1)
Computer Science - Distributed; Parallel; and Cluster Computing (1)

Publications Authored By Leslie Lamport


With state-based methods, checking that an implementation satisfies a higher-level specification requires describing how the higher-level concepts in the specification are represented by the lower-level data structures of the implementation. This approach was first proposed in the domain of sequential systems by Hoare in 1972. Hoare called the description an abstraction function. Read More

Affiliations: 1INRIA Paris-Rocquencourt, 2MSR - INRIA, 3MSR - INRIA, 4MSR - INRIA, 5INRIA Nancy - Grand Est / LORIA

We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic. Read More

TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs. Read More

Affiliations: 1INRIA Saclay - Ile de France, 2INRIA Rocquencourt, 3INRIA Lorraine, 4INRIA Lorraine

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. Read More

Affiliations: 1MRI, 2INRIA Rocquencourt, 3INRIA Lorraine - LORIA, 4INRIA Lorraine - LORIA

We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Read More

The distributed transaction commit problem requires reaching agreement on whether a transaction is committed or aborted. The classic Two-Phase Commit protocol blocks if the coordinator fails. Fault-tolerant consensus algorithms also reach agreement, but do not block whenever any majority of the processes are working. Read More