74 citations · 127 across the 10 of their papers we have counts for
10 papers
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
Igor Konnov, Markus Kuppe, Stephan Merz
Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their…
Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle
Ran Chen, Cyril Cohen, Jean-Jacques Levy +2
Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from gr…
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…
Encoding TLA+ set theory into many-sorted first-order logic
Stephan Merz, Hernán Vanzetto
We present an encoding of Zermelo-Fraenkel set theory into many-sorted first-order logic, the input language of state-of-the-art SMT solvers. This translation is the main component…
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.
TLA+ Proofs
Denis Cousineau, Damien Doligez, Leslie Lamport +3
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 wi…