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…