12 citations · 12 across the 2 of their papers we have counts for
2 papers
cs.PL2024
Validating Traces of Distributed Programs Against TLA+ Specifications
Horatiu Cirstea, Markus A. Kuppe, Benjamin Loillier +1
TLA+ is a formal language for specifying systems, including distributed algorithms, that is supported by powerful verification tools. In this work we present a framework for relati…
cs.LO2022★ 12 cited
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…