74 citations · 173 across the 9 of their papers we have counts for
4 papers · 1 filter
Auxiliary Variables in TLA+
Leslie Lamport, Stephan Merz
Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implem…
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
Damien Doligez, Jael Kriener, Leslie Lamport +2
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.
Verifying Safety Properties With the TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport +1
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 element…
A TLA+ Proof System
Kaustuv C. Chaudhuri, Damien Doligez, Leslie Lamport +1
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 l…